1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro, Floris van Doorn
  5  
  6  The (classical) real numbers ℝ. This is a direct construction
  7  from Cauchy sequences.
  8  -/
  9  import order.conditionally_complete_lattice data.real.cau_seq_completion
src         └──────────────────────────────────┘ └──────────────────────────┘
 10    algebra.archimedean order.bounds
src    └─────────────────┘ └──────────┘
 11  
 12  def real := @cau_seq.completion.Cauchy ℚ _ _ _ abs _
id                └───────────────────────┘        └─┘
src               └───────────────────────┘        └─┘
typ               └───────────────────────┘        └─┘
doc                                         
 13  notation `ℝ` := real
id                   └──┘
src                  └──┘
typ                  └──┘
 14  
 15  namespace real
 16  open cau_seq cau_seq.completion
 17  
 18  variables {x y : ℝ}
id                    
src                   
typ                   
 19  
 20  def of_rat (x : ℚ) : ℝ := of_rat x
id                           └────┘ 
src                          └────┘
typ                          └────┘ 
doc                  
 21  
 22  def mk (x : cau_seq ℚ abs) : ℝ := cau_seq.completion.mk x
id               └─────┘  └─┘        └───────────────────┘ 
src              └─────┘  └─┘        └───────────────────┘
typ              └─────┘  └─┘        └───────────────────┘ 
doc                      
 23  
 24  def comm_ring_aux : comm_ring ℝ := cau_seq.completion.comm_ring
id                       └───────┘     └──────────────────────────┘
src                      └───────┘     └──────────────────────────┘
typ                      └───────┘     └──────────────────────────┘
 25  
 26  instance : comm_ring ℝ := { ..comm_ring_aux }
id              └───────┘         └───────────┘
src             └───────┘         └───────────┘
typ             └───────┘         └───────────┘
 27  
 28  /- Extra instances to short-circuit type class resolution -/
 29  instance : ring ℝ               := by apply_instance
id              └──┘ 
src             └──┘                      └─────────────┘
typ             └──┘                      └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 30  instance : comm_semiring ℝ      := by apply_instance
id              └───────────┘ 
src             └───────────┘             └─────────────┘
typ             └───────────┘             └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 31  instance : semiring ℝ           := by apply_instance
id              └──────┘ 
src             └──────┘                  └─────────────┘
typ             └──────┘                  └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 32  instance : add_comm_group ℝ     := by apply_instance
id              └────────────┘ 
src             └────────────┘            └─────────────┘
typ             └────────────┘            └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 33  instance : add_group ℝ          := by apply_instance
id              └───────┘ 
src             └───────┘                 └─────────────┘
typ             └───────┘                 └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 34  instance : add_comm_monoid ℝ    := by apply_instance
id              └─────────────┘ 
src             └─────────────┘           └─────────────┘
typ             └─────────────┘           └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 35  instance : add_monoid ℝ         := by apply_instance
id              └────────┘ 
src             └────────┘                └─────────────┘
typ             └────────┘                └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 36  instance : add_left_cancel_semigroup ℝ := by apply_instance
id              └───────────────────────┘ 
src             └───────────────────────┘        └─────────────┘
typ             └───────────────────────┘        └─────────────┘
doc                                               └─────────────┘
txt                                               └─────────────┘
par                                               └─────────────┘
pid                                                             
st                                               └──────────────┘
 37  instance : add_right_cancel_semigroup ℝ := by apply_instance
id              └────────────────────────┘ 
src             └────────────────────────┘        └─────────────┘
typ             └────────────────────────┘        └─────────────┘
doc                                                └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
 38  instance : add_comm_semigroup ℝ := by apply_instance
id              └────────────────┘ 
src             └────────────────┘        └─────────────┘
typ             └────────────────┘        └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 39  instance : add_semigroup ℝ      := by apply_instance
id              └───────────┘ 
src             └───────────┘             └─────────────┘
typ             └───────────┘             └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 40  instance : comm_monoid ℝ        := by apply_instance
id              └─────────┘ 
src             └─────────┘               └─────────────┘
typ             └─────────┘               └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 41  instance : monoid ℝ             := by apply_instance
id              └────┘ 
src             └────┘                    └─────────────┘
typ             └────┘                    └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 42  instance : comm_semigroup ℝ     := by apply_instance
id              └────────────┘ 
src             └────────────┘            └─────────────┘
typ             └────────────┘            └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 43  instance : semigroup ℝ          := by apply_instance
id              └───────┘ 
src             └───────┘                 └─────────────┘
typ             └───────┘                 └─────────────┘
doc                                        └─────────────┘
txt                                        └─────────────┘
par                                        └─────────────┘
pid                                                      
st                                        └──────────────┘
 44  instance : inhabited ℝ := ⟨0⟩
id              └───────┘ 
src             └───────┘ 
typ             └───────┘ 
 45  
 46  theorem of_rat_sub (x y : ℚ) : of_rat (x - y) = of_rat x - of_rat y :=
id                                 └────┘       └────┘   └────┘ 
src                                └────┘         └────┘    └────┘
typ                                └────┘       └────┘   └────┘ 
doc                            
 47  congr_arg mk (const_sub _ _)
id   └───────┘ └┘  └───────┘
src  └───────┘ └┘  └───────┘
typ  └───────┘ └┘  └───────┘
 48  
 49  instance : has_lt ℝ :=
id              └────┘ 
src             └────┘ 
typ             └────┘ 
 50  ⟨λ x y, quotient.lift_on₂ x y (<) $
id         └───────────────┘   
src          └───────────────┘     
typ        └───────────────┘   
 51    λ f₁ g₁ f₂ g₂ hf hg, propext $
id       └┘ └┘ └┘ └┘ └┘ └┘  └─────┘
src                         └─────┘
typ      └┘ └┘ └┘ └┘ └┘ └┘  └─────┘
 52    ⟨λ h, lt_of_eq_of_lt (setoid.symm hf) (lt_of_lt_of_eq h hg),
id          └────────────┘  └─────────┘ └┘   └────────────┘  └┘
src          └────────────┘  └─────────┘      └────────────┘
typ         └────────────┘  └─────────┘ └┘   └────────────┘  └┘
 53     λ h, lt_of_eq_of_lt hf (lt_of_lt_of_eq h (setoid.symm hg))⟩⟩
id          └────────────┘ └┘  └────────────┘   └─────────┘ └┘
src          └────────────┘     └────────────┘    └─────────┘
typ         └────────────┘ └┘  └────────────┘   └─────────┘ └┘
 54  
 55  @[simp] theorem mk_lt {f g : cau_seq ℚ abs} : mk f < mk g ↔ f < g := iff.rfl
id                                └─────┘  └─┘    └┘   └┘         └─────┘
src                               └─────┘  └─┘    └┘    └┘            └─────┘
typ                               └─────┘  └─┘    └┘   └┘         └─────┘
doc    └──┘                               
 56  
 57  theorem mk_eq {f g : cau_seq ℚ abs} : mk f = mk g ↔ f ≈ g := mk_eq
id                        └─────┘  └─┘    └┘   └┘         └───┘
src                       └─────┘  └─┘    └┘    └┘            └───┘
typ                       └─────┘  └─┘    └┘   └┘         └───┘
doc                               
 58  
 59  theorem quotient_mk_eq_mk (f : cau_seq ℚ abs) : ⟦f⟧ = mk f := rfl
id                                  └─────┘  └─┘      └┘     └─┘
src                                 └─────┘  └─┘       └┘      └─┘
typ                                 └─────┘  └─┘      └┘     └─┘
doc                                         
 60  
 61  theorem mk_eq_mk {f : cau_seq ℚ abs} : cau_seq.completion.mk f = mk f := rfl
id                         └─────┘  └─┘    └───────────────────┘   └┘     └─┘
src                        └─────┘  └─┘    └───────────────────┘    └┘      └─┘
typ                        └─────┘  └─┘    └───────────────────┘   └┘     └─┘
doc                                
 62  
 63  @[simp] theorem mk_pos {f : cau_seq ℚ abs} : 0 < mk f ↔ pos f :=
id                               └─────┘  └─┘       └┘   └─┘ 
src                              └─────┘  └─┘       └┘    └─┘
typ                              └─────┘  └─┘       └┘   └─┘ 
doc    └──┘                                                 └─┘
 64  iff_of_eq (congr_arg pos (sub_zero f))
id   └───────┘  └───────┘ └─┘  └──────┘ 
src  └───────┘  └───────┘ └─┘  └──────┘
typ  └───────┘  └───────┘ └─┘  └──────┘ 
doc                       └─┘
 65  
 66  protected def le (x y : ℝ) : Prop := x < y ∨ x = y
id                                             
src                                              
typ                                            
 67  instance : has_le ℝ := ⟨real.le⟩
id              └────┘      └─────┘
src             └────┘      └─────┘
typ             └────┘      └─────┘
 68  
 69  @[simp] theorem mk_le {f g : cau_seq ℚ abs} : mk f ≤ mk g ↔ f ≤ g :=
id                                └─────┘  └─┘    └┘   └┘     
src                               └─────┘  └─┘    └┘    └┘      
typ                               └─────┘  └─┘    └┘   └┘     
doc    └──┘                               
 70  or_congr iff.rfl quotient.eq
id   └──────┘ └─────┘ └─────────┘
src  └──────┘ └─────┘ └─────────┘
typ  └──────┘ └─────┘ └─────────┘
 71  
 72  theorem add_lt_add_iff_left {a b : ℝ} (c : ℝ) : c + a < c + b ↔ a < b :=
id                                                           
src                                                              
typ                                                          
 73  quotient.induction_on₃ a b c (λ f g h,
id   └────────────────────┘         
src  └────────────────────┘
typ  └────────────────────┘         
 74    iff_of_eq (congr_arg pos $ by rw add_sub_add_left_eq_sub))
id     └───────┘  └───────┘ └─┘         └─────────────────────┘
src    └───────┘  └───────┘ └─┘      └─┘└─────────────────────┘
typ    └───────┘  └───────┘ └─┘      └─┘└─────────────────────┘
doc                         └─┘      └─┘
txt                                  └─┘
par                                  └─┘
pid                                    
st                                  └─────────────────────────┘
 75  
 76  instance : linear_order ℝ :=
id              └──────────┘ 
src             └──────────┘ 
typ             └──────────┘ 
 77  { le := (≤), lt := (<),
id                     
src                    
typ                    
 78    le_refl := λ a, or.inr rfl,
id                    └────┘ └─┘
src                    └────┘ └─┘
typ                   └────┘ └─┘
 79    le_trans := λ a b c, quotient.induction_on₃ a b c $
id                       └────────────────────┘   
src                         └────────────────────┘
typ                      └────────────────────┘   
 80      λ f g h, by simpa [quotient_mk_eq_mk] using le_trans,
id                       └───────────────┘        └──────┘
src                  └─────┘└───────────────┘└──────┘└──────┘
typ               └─────┘└───────────────┘└──────┘└──────┘
doc                  └─────┘                 └──────┘
txt                  └─────┘                 └──────┘
par                  └─────┘                 └──────┘
pid                                        └────┘
st                  └───────────────────────────────────────┘
 81    lt_iff_le_not_le := λ a b, quotient.induction_on₂ a b $
id                              └────────────────────┘  
src                               └────────────────────┘
typ                             └────────────────────┘  
 82      λ f g, by simpa [quotient_mk_eq_mk] using lt_iff_le_not_le,
id                      └───────────────┘        └──────────────┘
src                └─────┘└───────────────┘└──────┘└──────────────┘
typ              └─────┘└───────────────┘└──────┘└──────────────┘
doc                └─────┘                 └──────┘
txt                └─────┘                 └──────┘
par                └─────┘                 └──────┘
pid                                      └────┘
st                └───────────────────────────────────────────────┘
 83    le_antisymm := λ a b, quotient.induction_on₂ a b $
id                         └────────────────────┘  
src                          └────────────────────┘
typ                        └────────────────────┘  
 84      λ f g, by simpa [mk_eq, quotient_mk_eq_mk] using @cau_seq.le_antisymm _ _ f g,
id                      └───┘  └───────────────┘         └─────────────────┘      
src                └─────┘└───┘└┘└───────────────┘└──────┘ └─────────────────┘└───┘ 
typ              └─────┘└───┘└┘└───────────────┘└──────┘ └─────────────────┘└───┘
doc                └─────┘     └┘                 └──────┘                    └───┘ 
txt                └─────┘     └┘                 └──────┘                    └───┘ 
par                └─────┘     └┘                 └──────┘                    └───┘ 
pid                          └┘                 └────┘                    └───┘ 
st                └──────────────────────────────────────────────────────────────────┘
 85    le_total := λ a b, quotient.induction_on₂ a b $
id                      └────────────────────┘  
src                       └────────────────────┘
typ                     └────────────────────┘  
 86      λ f g, by simpa [quotient_mk_eq_mk] using le_total f g }
id                      └───────────────┘        └──────┘  
src                └─────┘└───────────────┘└──────┘└──────┘  
typ              └─────┘└───────────────┘└──────┘└──────┘
doc                └─────┘                 └──────┘          
txt                └─────┘                 └──────┘          
par                └─────┘                 └──────┘          
pid                                      └────┘          
st                └────────────────────────────────────────────┘
 87  
 88  instance : partial_order ℝ := by apply_instance
id              └───────────┘ 
src             └───────────┘        └─────────────┘
typ             └───────────┘        └─────────────┘
doc                                   └─────────────┘
txt                                   └─────────────┘
par                                   └─────────────┘
pid                                                 
st                                   └──────────────┘
 89  instance : preorder ℝ      := by apply_instance
id              └──────┘ 
src             └──────┘             └──────────────
typ             └──────┘             └──────────────
doc                                   └──────────────
txt                                   └──────────────
par                                   └──────────────
pid                                                 
st                                   └───────────────
 90  
src  
typ  
doc  
txt  
par  
pid  
st   
 91  theorem of_rat_lt {x y : ℚ} : of_rat x < of_rat y ↔ x < y := const_lt
id                                └────┘   └────┘         └──────┘
src                               └────┘    └────┘            └──────┘
typ                               └────┘   └────┘         └──────┘
doc                           
 92  
 93  protected theorem zero_lt_one : (0 : ℝ) < 1 := of_rat_lt.2 zero_lt_one
id                                                └───────┘  └─────────┘
src                                               └───────┘  └─────────┘
typ                                               └───────┘  └─────────┘
 94  
 95  protected theorem mul_pos {a b : ℝ} : 0 < a → 0 < b → 0 < a * b :=
id                                                         
src                                                          
typ                                                        
 96  quotient.induction_on₂ a b $ λ f g,
id   └────────────────────┘        
src  └────────────────────┘
typ  └────────────────────┘        
 97    show pos (f - 0) → pos (g - 0) → pos (f * g - 0),
id          └─┘        └─┘         └─┘     
src         └─┘          └─┘          └─┘       
typ         └─┘        └─┘         └─┘     
doc         └─┘           └─┘           └─┘
 98    by simpa using cau_seq.mul_pos
id                    └─────────────┘
src       └──────────┘└─────────────┘
typ       └──────────┘└─────────────┘
doc       └──────────┘               
txt       └──────────┘               
par       └──────────┘               
pid            └────┘               
st       └────────────────────────────
 99  
src  
typ  
doc  
txt  
par  
pid  
st   
100  instance : linear_ordered_comm_ring ℝ :=
id              └──────────────────────┘ 
src             └──────────────────────┘ 
typ             └──────────────────────┘ 
101  { add_le_add_left := λ a b h c,
id                             
typ                            
102      (le_iff_le_iff_lt_iff_lt.2 $ real.add_lt_add_iff_left c).2 h,
id        └─────────────────────┘    └──────────────────────┘    
src       └─────────────────────┘    └──────────────────────┘   
typ       └─────────────────────┘    └──────────────────────┘    
103    zero_ne_one := ne_of_lt real.zero_lt_one,
id                    └──────┘ └──────────────┘
src                   └──────┘ └──────────────┘
typ                   └──────┘ └──────────────┘
104    mul_nonneg := λ a b a0 b0,
id                       └┘ └┘
typ                      └┘ └┘
105      match a0, b0 with
id             └┘  └┘
typ            └┘  └┘
106      | or.inl a0, or.inl b0 := le_of_lt (real.mul_pos a0 b0)
id                └┘  └────┘ └┘    └──────┘  └──────────┘
src                   └────┘       └──────┘  └──────────┘
typ               └┘  └────┘ └┘    └──────┘  └──────────┘
107      | or.inr a0, _ := by simp [a0.symm]
id         └────┘
src        └────┘             └────┘       └─
typ        └────┘             └────┘└─────┘└─
doc                           └────┘       └─
txt                           └────┘       └─
par                           └────┘       └─
pid                                      
st                           └───────────────
108      | _, or.inr b0 := by simp [b0.symm]
id            └────┘
src  ───┘     └────┘          └────┘       └─
typ  ───┘     └────┘          └────┘└─────┘└─
doc  ───┘                     └────┘       └─
txt  ───┘                     └────┘       └─
par  ───┘                     └────┘       └─
pid  ───┘                                
st   ───┘                    └───────────────
109      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
110    mul_pos := @real.mul_pos,
id                 └──────────┘
src                └──────────┘
typ                └──────────┘
111    zero_lt_one := real.zero_lt_one,
id                    └──────────────┘
src                   └──────────────┘
typ                   └──────────────┘
112    add_lt_add_left := λ a b h c, (real.add_lt_add_iff_left c).2 h,
id                                └──────────────────────┘    
src                                   └──────────────────────┘   
typ                               └──────────────────────┘    
113    ..real.comm_ring, ..real.linear_order }
id       └────────────┘    └───────────────┘
src      └────────────┘    └───────────────┘
typ      └────────────┘    └───────────────┘
114  
115  /- Extra instances to short-circuit type class resolution -/
116  instance : linear_ordered_ring ℝ        := by apply_instance
id              └─────────────────┘ 
src             └─────────────────┘               └─────────────┘
typ             └─────────────────┘               └─────────────┘
doc                                                └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
117  instance : ordered_ring ℝ               := by apply_instance
id              └──────────┘ 
src             └──────────┘                      └─────────────┘
typ             └──────────┘                      └─────────────┘
doc                                                └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
118  instance : linear_ordered_semiring ℝ    := by apply_instance
id              └─────────────────────┘ 
src             └─────────────────────┘           └─────────────┘
typ             └─────────────────────┘           └─────────────┘
doc                                                └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
119  instance : ordered_semiring ℝ           := by apply_instance
id              └──────────────┘ 
src             └──────────────┘                  └─────────────┘
typ             └──────────────┘                  └─────────────┘
doc                                                └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
120  instance : ordered_comm_group ℝ         := by apply_instance
id              └────────────────┘ 
src             └────────────────┘                └─────────────┘
typ             └────────────────┘                └─────────────┘
doc                                                └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
121  instance : ordered_cancel_comm_monoid ℝ := by apply_instance
id              └────────────────────────┘ 
src             └────────────────────────┘        └─────────────┘
typ             └────────────────────────┘        └─────────────┘
doc                                                └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
122  instance : ordered_comm_monoid ℝ        := by apply_instance
id              └─────────────────┘ 
src             └─────────────────┘               └─────────────┘
typ             └─────────────────┘               └─────────────┘
doc             └─────────────────┘                └─────────────┘
txt                                                └─────────────┘
par                                                └─────────────┘
pid                                                              
st                                                └──────────────┘
123  instance : domain ℝ                     := by apply_instance
id              └────┘ 
src             └────┘                            └──────────────
typ             └────┘                            └──────────────
doc             └────┘                             └──────────────
txt                                                └──────────────
par                                                └──────────────
pid                                                              
st                                                └───────────────
124  
src  
typ  
doc  
txt  
par  
pid  
st   
125  open_locale classical
126  
127  noncomputable instance : discrete_linear_ordered_field ℝ :=
id                            └───────────────────────────┘ 
src                           └───────────────────────────┘ 
typ                           └───────────────────────────┘ 
128  { decidable_le := by apply_instance,
src                       └────────────┘
typ                       └────────────┘
doc                       └────────────┘
txt                       └────────────┘
par                       └────────────┘
st                       └─────────────┘
129    ..real.linear_ordered_comm_ring,
id       └───────────────────────────┘
src      └───────────────────────────┘
typ      └───────────────────────────┘
130    ..real.domain,
id       └─────────┘
src      └─────────┘
typ      └─────────┘
131    ..cau_seq.completion.discrete_field }
id       └───────────────────────────────┘
src      └───────────────────────────────┘
typ      └───────────────────────────────┘
132  
133  /- Extra instances to short-circuit type class resolution -/
134  
135  noncomputable instance : linear_ordered_field ℝ    := by apply_instance
id                            └──────────────────┘ 
src                           └──────────────────┘           └─────────────┘
typ                           └──────────────────┘           └─────────────┘
doc                                                           └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
136  noncomputable instance : decidable_linear_ordered_comm_ring ℝ := by apply_instance
id                            └────────────────────────────────┘ 
src                           └────────────────────────────────┘        └─────────────┘
typ                           └────────────────────────────────┘        └─────────────┘
doc                                                                      └─────────────┘
txt                                                                      └─────────────┘
par                                                                      └─────────────┘
pid                                                                                    
st                                                                      └──────────────┘
137  noncomputable instance : decidable_linear_ordered_semiring ℝ := by apply_instance
id                            └───────────────────────────────┘ 
src                           └───────────────────────────────┘        └─────────────┘
typ                           └───────────────────────────────┘        └─────────────┘
doc                                                                     └─────────────┘
txt                                                                     └─────────────┘
par                                                                     └─────────────┘
pid                                                                                   
st                                                                     └──────────────┘
138  noncomputable instance : decidable_linear_ordered_comm_group ℝ := by apply_instance
id                            └─────────────────────────────────┘ 
src                           └─────────────────────────────────┘        └─────────────┘
typ                           └─────────────────────────────────┘        └─────────────┘
doc                                                                       └─────────────┘
txt                                                                       └─────────────┘
par                                                                       └─────────────┘
pid                                                                                     
st                                                                       └──────────────┘
139  noncomputable instance discrete_field : discrete_field ℝ := by apply_instance
id                                           └────────────┘ 
src                                          └────────────┘        └─────────────┘
typ                                          └────────────┘        └─────────────┘
doc                                                                 └─────────────┘
txt                                                                 └─────────────┘
par                                                                 └─────────────┘
pid                                                                               
st                                                                 └──────────────┘
140  noncomputable instance : field ℝ                   := by apply_instance
id                            └───┘ 
src                           └───┘                          └─────────────┘
typ                           └───┘                          └─────────────┘
doc                                                           └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
141  noncomputable instance : division_ring ℝ           := by apply_instance
id                            └───────────┘ 
src                           └───────────┘                  └─────────────┘
typ                           └───────────┘                  └─────────────┘
doc                                                           └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
142  noncomputable instance : integral_domain ℝ         := by apply_instance
id                            └─────────────┘ 
src                           └─────────────┘                └─────────────┘
typ                           └─────────────┘                └─────────────┘
doc                                                           └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
143  noncomputable instance : nonzero_comm_ring ℝ       := by apply_instance
id                            └───────────────┘ 
src                           └───────────────┘              └─────────────┘
typ                           └───────────────┘              └─────────────┘
doc                           └───────────────┘               └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
144  noncomputable instance : decidable_linear_order ℝ  := by apply_instance
id                            └────────────────────┘ 
src                           └────────────────────┘         └─────────────┘
typ                           └────────────────────┘         └─────────────┘
doc                                                           └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
145  noncomputable instance : lattice.distrib_lattice ℝ := by apply_instance
id                            └─────────────────────┘ 
src                           └─────────────────────┘        └─────────────┘
typ                           └─────────────────────┘        └─────────────┘
doc                           └─────────────────────┘         └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
146  noncomputable instance : lattice.lattice ℝ         := by apply_instance
id                            └─────────────┘ 
src                           └─────────────┘                └─────────────┘
typ                           └─────────────┘                └─────────────┘
doc                           └─────────────┘                 └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
147  noncomputable instance : lattice.semilattice_inf ℝ := by apply_instance
id                            └─────────────────────┘ 
src                           └─────────────────────┘        └─────────────┘
typ                           └─────────────────────┘        └─────────────┘
doc                           └─────────────────────┘         └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
148  noncomputable instance : lattice.semilattice_sup ℝ := by apply_instance
id                            └─────────────────────┘ 
src                           └─────────────────────┘        └─────────────┘
typ                           └─────────────────────┘        └─────────────┘
doc                           └─────────────────────┘         └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
149  noncomputable instance : lattice.has_inf ℝ         := by apply_instance
id                            └─────────────┘ 
src                           └─────────────┘                └─────────────┘
typ                           └─────────────┘                └─────────────┘
doc                           └─────────────┘                 └─────────────┘
txt                                                           └─────────────┘
par                                                           └─────────────┘
pid                                                                         
st                                                           └──────────────┘
150  noncomputable instance : lattice.has_sup ℝ         := by apply_instance
id                            └─────────────┘ 
src                           └─────────────┘                └──────────────
typ                           └─────────────┘                └──────────────
doc                           └─────────────┘                 └──────────────
txt                                                           └──────────────
par                                                           └──────────────
pid                                                                         
st                                                           └───────────────
151  
src  
typ  
doc  
txt  
par  
pid  
st   
152  lemma le_of_forall_epsilon_le {a b : real} (h : ∀ε, ε > 0 → a ≤ b + ε) : a ≤ b :=
id                                        └──┘                          
src                                       └──┘                               
typ                                       └──┘                          
153  le_of_forall_le_of_dense $ assume x hxb,
id   └──────────────────────┘           └─┘
src  └──────────────────────┘
typ  └──────────────────────┘           └─┘
154  calc  a ≤ b + (x - b) : h (x-b) $ sub_pos.2 hxb
id                           └─────┘  └─┘
src                                 └─────┘
typ                          └─────┘  └─┘
155      ... = x : by rw [add_comm]; simp
id                       └──────┘
src                   └──┘└──────┘  └────
typ                  └──┘└──────┘  └────
doc                   └──┘          └────
txt                   └──┘          └────
par                   └──┘          └────
pid                     └┘              
st                   └───────────┘└──────
156  
src  
typ  
doc  
txt  
par  
pid  
st   
157  open rat
158  
159  @[simp] theorem of_rat_eq_cast : ∀ x : ℚ, of_rat x = x :=
id                                            └────┘   
src                                           └────┘   
typ                                           └────┘   
doc    └──┘                                 
160  eq_cast of_rat rfl of_rat_add of_rat_mul
id   └─────┘ └────┘ └─┘ └────────┘ └────────┘
src  └─────┘ └────┘ └─┘ └────────┘ └────────┘
typ  └─────┘ └────┘ └─┘ └────────┘ └────────┘
161  
162  theorem le_mk_of_forall_le {f : cau_seq ℚ abs} :
id                                   └─────┘  └─┘
src                                  └─────┘  └─┘
typ                                  └─────┘  └─┘
doc                                          
163    (∃ i, ∀ j ≥ i, x ≤ f j) → x ≤ mk f :=
id                        └┘ 
src                             └┘
typ                       └┘ 
164  quotient.induction_on x $ λ g h, le_of_not_lt $
id   └───────────────────┘         └──────────┘
src  └───────────────────┘            └──────────┘
typ  └───────────────────┘         └──────────┘
165  λ ⟨K, K0, hK⟩,
id        └┘  └┘
typ       └┘  └┘
166  let ⟨i, H⟩ := exists_forall_ge_and h $
id   └─┘           └──────────────────┘ 
src                └──────────────────┘
typ  └─┘           └──────────────────┘ 
167    exists_forall_ge_and hK (f.cauchy₃ $ half_pos K0) in
id     └──────────────────┘     └──────┘   └──────┘
src    └──────────────────┘      └──────┘   └──────┘
typ    └──────────────────┘     └──────┘   └──────┘
168  begin
st   └─────
169    apply not_lt_of_le (H _ (le_refl _)).1,
id           └──────────┘      └─────┘
src    └────┘└──────────┘  └─┘ └─────┘└────┘
typ    └────┘└──────────┘ └─┘ └─────┘└────┘
doc    └────┘              └─┘        └────┘
txt    └────┘              └─┘        └────┘
par    └────┘              └─┘        └────┘
pid                       └─┘        └──┘└┘
st   ───────────────────────────────────────┘└─
170    rw ← of_rat_eq_cast,
id          └────────────┘
src    └───┘└────────────┘
typ    └───┘└────────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ────────────────────┘└─
171    refine ⟨_, half_pos K0, i, λ j ij, _⟩,
id                └──────┘ └┘  
src    └─────┘ └─┘└──────┘  └┘ └┘ └───────┘
typ    └─────┘ └─┘└──────┘└┘└┘└┘ └───────┘
doc    └─────┘ └─┘          └┘ └┘ └───────┘
txt    └─────┘ └─┘          └┘ └┘ └───────┘
par    └─────┘ └─┘          └┘ └┘ └───────┘
pid           └─┘          └┘ └┘ └───────┘
st   ──────────────────────────────────────┘└─
172    have := add_le_add (H _ ij).2.1
id             └────────┘
src    └──────┘└────────┘  └─┘  └─────
typ    └──────┘└────────┘  └─┘  └─────
doc    └──────┘            └─┘  └─────
txt    └──────┘            └─┘  └─────
par    └──────┘            └─┘  └─────
pid    └───┘└─┘            └─┘  └─────
st   ──────────────────────────────────
173      (le_of_lt (abs_lt.1 $ (H _ (le_refl _)).2.2 _ ij).1),
id        └──────┘  └────┘          └─────┘           └┘
src  ───┘ └──────┘ └────┘└─┘   └─┘ └─────┘└─────────┘  └──┘
typ  ───┘ └──────┘ └────┘└─┘  └─┘ └─────┘└─────────┘└┘└──┘
doc  ───┘                └─┘   └─┘        └─────────┘  └──┘
txt  ───┘                └─┘   └─┘        └─────────┘  └──┘
par  ───┘                └─┘   └─┘        └─────────┘  └──┘
pid  ───┘                └─┘   └─┘        └─────────┘  └──┘
st   ───────────────────────────────────────────────────────┘└─
174    rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this
id            └────────────┘  └──────────────┘  └───────┘  └────────────────┘
src    └─────┘└────────────┘└┘└──────────────┘└┘└───────┘└┘└────────────────┘└────────┘
typ    └─────┘└────────────┘└┘└──────────────┘└┘└───────┘└┘└────────────────┘└────────┘
doc    └─────┘              └┘                └┘         └┘                  └────────┘
txt    └─────┘              └┘                └┘         └┘                  └────────┘
par    └─────┘              └┘                └┘         └┘                  └────────┘
pid       └──┘              └┘                └┘         └┘                  └──────┘
st   ──────────────────────┘└────────────────┘└─────────┘└──────────────────┘└───────┘
175  end
st   └─┘
176  
177  theorem mk_le_of_forall_le {f : cau_seq ℚ abs} {x : ℝ} :
id                                   └─────┘  └─┘       
src                                  └─────┘  └─┘       
typ                                  └─────┘  └─┘       
doc                                          
178    (∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) → mk f ≤ x
id                          └┘   
src                                └┘   
typ                         └┘   
179  | ⟨i, H⟩ := by rw [← neg_le_neg_iff, ← mk_eq_mk, mk_neg]; exact
id                        └────────────┘    └──────┘  └────┘
src                 └────┘└────────────┘└──┘└──────┘└┘└────┘  └─────
typ                 └────┘└────────────┘└──┘└──────┘└┘└────┘  └─────
doc                 └────┘              └──┘        └┘        └─────
txt                 └────┘              └──┘        └┘        └─────
par                 └────┘              └──┘        └┘        └─────
pid                   └──┘              └──┘        └┘             
st                 └───────────────────┘└──────────┘└──────┘└───────
180    le_mk_of_forall_le ⟨i, λ j ij, by simp [H _ ij]⟩
id     └────────────────┘                        └┘
src  ─┘└────────────────┘  └┘ └─────┘  └────┘ └─┘  └─
typ  ─┘└────────────────┘ └┘ └─────┘  └────┘└─┘└┘└─
doc  ─┘                    └┘ └─────┘  └────┘ └─┘  └─
txt  ─┘                    └┘ └─────┘  └────┘ └─┘  └─
par  ─┘                    └┘ └─────┘  └────┘ └─┘  └─
pid  ─┘                    └┘ └─────┘  └─────┘ └─┘  └┘
st   ──────────────────────────────────┘└────────────┘└─
181  
src  
typ  
doc  
txt  
par  
pid  
st   
182  theorem mk_near_of_forall_near {f : cau_seq ℚ abs} {x : ℝ} {ε : ℝ}
id                                       └─────┘  └─┘              
src                                      └─────┘  └─┘              
typ                                      └─────┘  └─┘              
doc                                              
183    (H : ∃ i, ∀ j ≥ i, abs ((f j : ℝ) - x) ≤ ε) : abs (mk f - x) ≤ ε :=
id                   └─┘                 └─┘  └┘      
src                     └─┘                     └─┘  └┘       
typ                  └─┘                 └─┘  └┘      
184  abs_sub_le_iff.2
id   └────────────┘
src  └────────────┘
typ  └────────────┘
185    ⟨sub_le_iff_le_add'.2 $ mk_le_of_forall_le $
id      └────────────────┘    └────────────────┘
src     └────────────────┘    └────────────────┘
typ     └────────────────┘    └────────────────┘
186      H.imp $ λ i h j ij, sub_le_iff_le_add'.1 (abs_sub_le_iff.1 $ h j ij).1,
id       └──┘        └┘  └────────────────┘   └────────────┘      └┘ 
src       └──┘               └────────────────┘   └────────────┘           
typ      └──┘        └┘  └────────────────┘   └────────────┘      └┘ 
187    sub_le.1 $ le_mk_of_forall_le $
id     └────┘    └────────────────┘
src    └────┘    └────────────────┘
typ    └────┘    └────────────────┘
188      H.imp $ λ i h j ij, sub_le.1 (abs_sub_le_iff.1 $ h j ij).2⟩
id       └──┘        └┘  └────┘   └────────────┘      └┘ 
src       └──┘               └────┘   └────────────┘           
typ      └──┘        └┘  └────┘   └────────────┘      └┘ 
189  
190  instance : archimedean ℝ :=
id              └─────────┘ 
src             └─────────┘ 
typ             └─────────┘ 
191  archimedean_iff_rat_le.2 $ λ x, quotient.induction_on x $ λ f,
id   └────────────────────┘        └───────────────────┘      
src  └────────────────────┘         └───────────────────┘
typ  └────────────────────┘        └───────────────────┘      
192  let ⟨M, M0, H⟩ := f.bounded' 0 in
id   └─┘             └───────┘
src                     └───────┘
typ  └─┘             └───────┘
193  ⟨M, mk_le_of_forall_le ⟨0, λ i _,
id       └────────────────┘        
src      └────────────────┘
typ      └────────────────┘        
194    rat.cast_le.2 $ le_of_lt (abs_lt.1 (H i)).2⟩⟩
id     └─────────┘    └──────┘  └────┘       
src    └─────────┘    └──────┘  └────┘        
typ    └─────────┘    └──────┘  └────┘       
195  
196  /- mark `real` irreducible in order to prevent `auto_cases` unfolding reals,
197  since users rarely want to consider real numbers as Cauchy sequences.
198  Marking `comm_ring_aux` `irreducible` is done to ensure that there are no problems
199  with non definitionally equal instances, caused by making `real` irreducible-/
200  attribute [irreducible] real comm_ring_aux
id                           └──┘ └───────────┘
src                          └──┘ └───────────┘
typ                          └──┘ └───────────┘
doc             └─────────┘
201  
202  noncomputable instance : floor_ring ℝ := archimedean.floor_ring _
id                            └────────┘     └────────────────────┘
src                           └────────┘     └────────────────────┘
typ                           └────────┘     └────────────────────┘
doc                           └────────┘
203  
204  theorem is_cau_seq_iff_lift {f : ℕ → ℚ} : is_cau_seq abs f ↔ is_cau_seq abs (λ i, (f i : ℝ)) :=
id                                           └────────┘ └─┘   └────────┘ └─┘           
src                                          └────────┘ └─┘    └────────┘ └─┘              
typ                                          └────────┘ └─┘   └────────┘ └─┘           
doc                                           └────────┘         └────────┘
205  ⟨λ H ε ε0,
id        └┘
typ       └┘
206    let ⟨δ, δ0, δε⟩ := exists_pos_rat_lt ε0 in
id     └─┘     └┘  └┘     └───────────────┘ └┘
src                       └───────────────┘
typ    └─┘     └┘  └┘     └───────────────┘ └┘
207    (H _ δ0).imp $ λ i hi j ij, lt_trans
id            └─┘       └┘  └┘  └──────┘
src            └─┘                 └──────┘
typ           └─┘       └┘  └┘  └──────┘
208      (by simpa using (@rat.cast_lt ℝ _ _ _).2 (hi _ ij)) δε,
id                         └─────────┘             └┘   └┘
src          └──────────┘  └─────────┘ └────────┘   └─┘  
typ          └──────────┘  └─────────┘ └────────┘ └┘└─┘└┘
doc          └──────────┘              └────────┘   └─┘  
txt          └──────────┘              └────────┘   └─┘  
par          └──────────┘              └────────┘   └─┘  
pid               └────┘              └────────┘   └─┘  
st          └─────────────────────────────────────────────┘
209   λ H ε ε0, (H _ (rat.cast_pos.2 ε0)).imp $
id        └┘       └──────────┘  └┘  └─┘
src                   └──────────┘      └─┘
typ       └┘       └──────────┘  └┘  └─┘
210     λ i hi j ij, (@rat.cast_lt ℝ _ _ _).1 $ by simpa using hi _ ij⟩
id         └┘  └┘    └─────────┘                           └┘   └┘
src                    └─────────┘               └──────────┘  └─┘
typ        └┘  └┘    └─────────┘               └──────────┘└┘└─┘└┘
doc                                                └──────────┘  └─┘
txt                                                └──────────┘  └─┘
par                                                └──────────┘  └─┘
pid                                                     └────┘  └─┘
st                                                └──────────────────┘
211  
212  theorem of_near (f : ℕ → ℚ) (x : ℝ)
id                                  
src                                 
typ                                 
doc                           
213    (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abs ((f j : ℝ) - x) < ε) :
id                           └─┘             
src                             └─┘               
typ                          └─┘             
214    ∃ h', real.mk ⟨f, h'⟩ = x :=
id      └┘ └─────┘    └┘   
src        └─────┘         
typ     └┘ └─────┘    └┘   
215  ⟨is_cau_seq_iff_lift.2 (of_near _ (const abs x) h),
id    └─────────────────┘   └─────┘    └───┘ └─┘   
src   └─────────────────┘   └─────┘    └───┘ └─┘
typ   └─────────────────┘   └─────┘    └───┘ └─┘   
doc                                     └───┘
216   sub_eq_zero.1 $ abs_eq_zero.1 $
id    └─────────┘    └─────────┘
src   └─────────┘    └─────────┘
typ   └─────────┘    └─────────┘
217    eq_of_le_of_forall_le_of_dense (abs_nonneg _) $ λ ε ε0,
id     └────────────────────────────┘  └────────┘         └┘
src    └────────────────────────────┘  └────────┘
typ    └────────────────────────────┘  └────────┘         └┘
218      mk_near_of_forall_near $
id       └────────────────────┘
src      └────────────────────┘
typ      └────────────────────┘
219      (h _ ε0).imp (λ i h j ij, le_of_lt (h j ij))⟩
id           └┘ └─┘        └┘  └──────┘    └┘
src              └─┘               └──────┘
typ          └┘ └─┘        └┘  └──────┘    └┘
220  
221  theorem exists_floor (x : ℝ) : ∃ (ub : ℤ), (ub:ℝ) ≤ x ∧
id                                           └┘     
src                                                  
typ                                          └┘     
222     ∀ (z : ℤ), (z:ℝ) ≤ x → z ≤ ub :=
id                          └┘
src                           
typ                         └┘
223  int.exists_greatest_of_bdd
id   └────────────────────────┘
src  └────────────────────────┘
typ  └────────────────────────┘
224    (let ⟨n, hn⟩ := exists_int_gt x in ⟨n, λ z h',
id      └─┘    └┘     └───────────┘            └┘
src                    └───────────┘
typ     └─┘    └┘     └───────────┘            └┘
225      int.cast_le.1 $ le_trans h' $ le_of_lt hn⟩)
id       └─────────┘    └──────┘ └┘   └──────┘
src      └─────────┘    └──────┘      └──────┘
typ      └─────────┘    └──────┘ └┘   └──────┘
226    (let ⟨n, hn⟩ := exists_int_lt x in ⟨n, le_of_lt hn⟩)
id      └─┘    └┘     └───────────┘         └──────┘
src                    └───────────┘          └──────┘
typ     └─┘    └┘     └───────────┘         └──────┘
227  
228  theorem exists_sup (S : set ℝ) : (∃ x, x ∈ S) → (∃ x, ∀ y ∈ S, y ≤ x) →
id                           └─┘                         
src                          └─┘                               
typ                          └─┘                         
229    ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y
id                        
src                             
typ                       
230  | ⟨L, hL⟩ ⟨U, hU⟩ := begin
st                        └─────
231    choose f hf using begin
src    └────────────────┘     
typ    └────────────────┘     
doc    └────────────────┘     
txt    └────────────────┘     
par    └────────────────┘     
pid          └┘└─┘└─────┘     
st   ───────────────────┘└─────
232      refine λ d : ℕ, @int.exists_greatest_of_bdd
id                        └────────────────────────┘
src  ───┘└─────┘ └───┘ └┘ └────────────────────────┘
typ  ───┘└─────┘ └───┘ └┘ └────────────────────────┘
doc  ───┘└─────┘ └───┘ └┘                           
txt  ───┘└─────┘ └───┘ └┘                           
par  ───┘└─────┘ └───┘ └┘                           
pid  ──────────┘ └───┘ └┘                           
st   ────────────────────────────────────────────────
233        (λ n, ∃ y ∈ S, (n:ℝ) ≤ y * d) _ _ _,
id                              
src  ─────┘  └──┘└───┘    └┘  └─────┘└─
typ  ─────┘  └──┘└───┘   └┘  └─────┘└─
doc  ─────┘  └──┘ └───┘     └┘    └─────┘└─
txt  ─────┘  └──┘ └───┘     └┘    └─────┘└─
par  ─────┘  └──┘ └───┘     └┘    └─────┘└─
pid  ─────┘  └──┘ └───┘     └┘    └────────
st   ────────────────────────────────────────┘└─
234      { cases exists_int_gt U with k hk,
id               └───────────┘ 
src  ─────┘└────┘└───────────┘ └────────┘└─
typ  ─────┘└────┘└───────────┘└────────┘└─
doc  ─────┘└────┘              └────────┘└─
txt  ─────┘└────┘              └────────┘└─
par  ─────┘└────┘              └────────┘└─
pid  ───────────┘              └───────────
st   ────┘└──────────────────────────────┘└─
235        refine ⟨k * d, λ z h, _⟩,
id                    
src  ─────┘└─────┘    └┘ └──────┘└─
typ  ─────┘└─────┘  └┘ └──────┘└─
doc  ─────┘└─────┘    └┘ └──────┘└─
txt  ─────┘└─────┘    └┘ └──────┘└─
par  ─────┘└─────┘    └┘ └──────┘└─
pid  ────────────┘    └┘ └─────────
st   ─────────────────────────────┘└─
236        rcases h with ⟨y, yS, hy⟩,
id                
src  ─────┘└─────┘ └───────────────┘└─
typ  ─────┘└─────┘└───────────────┘└─
doc  ─────┘└─────┘ └───────────────┘└─
txt  ─────┘└─────┘ └───────────────┘└─
par  ─────┘└─────┘ └───────────────┘└─
pid  ────────────┘ └──────────────────
st   ──────────────────────────────┘└─
237        refine int.cast_le.1 (le_trans hy _),
id                └─────────┘    └──────┘ └┘
src  ─────┘└─────┘└─────────┘└─┘ └──────┘  └─┘└─
typ  ─────┘└─────┘└─────────┘└─┘ └──────┘└┘└─┘└─
doc  ─────┘└─────┘           └─┘           └─┘└─
txt  ─────┘└─────┘           └─┘           └─┘└─
par  ─────┘└─────┘           └─┘           └─┘└─
pid  ────────────┘           └─┘           └────
st   ─────────────────────────────────────────┘└─
238        simp,
src  ─────┘└──┘└─
typ  ─────┘└──┘└─
doc  ─────┘└──┘└─
txt  ─────┘└──┘└─
par  ─────┘└──┘└─
pid  ────────────
st   ─────────┘└─
239        exact mul_le_mul_of_nonneg_right
id               └────────────────────────┘
src  ─────┘└────┘└────────────────────────┘
typ  ─────┘└────┘└────────────────────────┘
doc  ─────┘└────┘                          
txt  ─────┘└────┘                          
par  ─────┘└────┘                          
pid  ───────────┘                          
st   ───────────────────────────────────────
240          (le_trans (hU _ yS) (le_of_lt hk)) (nat.cast_nonneg _) },
id            └──────┘  └┘   └┘   └──────┘ └┘    └─────────────┘
src  ───────┘ └──────┘   └─┘  └┘ └──────┘  └─┘ └─────────────┘└──┘└──
typ  ───────┘ └──────┘ └┘└─┘└┘└┘ └──────┘└┘└─┘ └─────────────┘└──┘└──
doc  ───────┘            └─┘  └┘           └─┘                └──┘└──
txt  ───────┘            └─┘  └┘           └─┘                └──┘└──
par  ───────┘            └─┘  └┘           └─┘                └──┘└──
pid  ───────┘            └─┘  └┘           └─┘                └──────
st   ──────────────────────────────────────────────────────────────┘└─
241      { exact ⟨⌊L * d⌋, L, hL, floor_le _⟩ }
id                        └┘  └──────┘
src  ─────┘└────┘    └┘ └┘  └┘└──────┘└──┘└─
typ  ─────┘└────┘   └┘└┘└┘└┘└──────┘└──┘└─
doc  ─────┘└────┘    └┘ └┘  └┘        └──┘└─
txt  ─────┘└────┘      └┘ └┘  └┘        └──┘└─
par  ─────┘└────┘      └┘ └┘  └┘        └──┘└─
pid  ───────────┘      └┘ └┘  └┘        └─────
st   ────────────────────────────────────────┘└─
242    end,
src  ────┘
typ  ────┘
doc  ────┘
txt  ────┘
par  ────┘
pid  ────┘
st   ────┘└─
243    have hf₁ : ∀ n > 0, ∃ y ∈ S, ((f n / n:ℚ):ℝ) ≤ y := λ n n0,
id                                    
src    └─────────┘ └────┘ └───┘       └┘ └┘  └──┘ └──────
typ    └─────────┘ └────┘ └───┘     └┘ └┘  └──┘ └──────
doc    └─────────┘ └────┘  └───┘         └┘ └┘  └──┘ └──────
txt    └─────────┘ └────┘  └───┘         └┘ └┘  └──┘ └──────
par    └─────────┘ └────┘  └───┘         └┘ └┘  └──┘ └──────
pid    └──────┘└─┘ └────┘  └───┘         └┘ └┘  └──┘ └──────
st   ──────────────────────────────────────────────────────────────
244      let ⟨y, yS, hy⟩ := (hf n).1 in
id              └┘          └┘
src  ───┘     └┘  └┘  └───┘    └──────
typ  ───┘    └┘└┘└┘  └───┘ └┘ └──────
doc  ───┘     └┘  └┘  └───┘    └──────
txt  ───┘     └┘  └┘  └───┘    └──────
par  ───┘     └┘  └┘  └───┘    └──────
pid  ───┘     └┘  └┘  └───┘    └──────
st   ───────────────────────────────────
245      ⟨y, yS, by simpa using (div_le_iff ((nat.cast_pos.2 n0):((_:ℝ) < _))).2 hy⟩,
id                               └────────┘   └──────────┘   └┘                 └┘
src  ───┘  └┘  └┘  └──────────┘ └────────┘  └──────────┘└─┘  └┘  └┘ └┘└──────┘  
typ  ───┘  └┘  └┘  └──────────┘ └────────┘  └──────────┘└─┘└┘└┘  └┘ └┘└──────┘└┘
doc  ───┘  └┘  └┘  └──────────┘                         └─┘  └┘  └┘ └┘ └──────┘  
txt  ───┘  └┘  └┘  └──────────┘                         └─┘  └┘  └┘ └┘ └──────┘  
par  ───┘  └┘  └┘  └──────────┘                         └─┘  └┘  └┘ └┘ └──────┘  
pid  ───┘  └┘  └┘  └───────────┘                         └─┘  └┘  └┘ └┘ └──────┘  
st   ─────────────┘└──────────────────────────────────────────────────────────────┘└─
246    have hf₂ : ∀ (n > 0) (y ∈ S), (y - (n:ℕ)⁻¹ : ℝ) < (f n / n:ℚ),
id                                          └┘         
src    └─────────┘ └────────────┘       └┘└─┘ └┘       
typ    └─────────┘ └────────────┘     └┘└─┘ └┘      
doc    └─────────┘ └────────────┘          └─┘ └┘       
txt    └─────────┘ └────────────┘          └─┘ └┘       
par    └─────────┘ └────────────┘          └─┘ └┘       
pid    └──────┘└─┘ └────────────┘          └─┘ └┘       
st   ──────────────────────────────────────────────────────────────┘└─
247    { intros n n0 y yS,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───┘└──────────────┘└─
248      have := lt_of_lt_of_le (sub_one_lt_floor _)
id               └────────────┘  └──────────────┘
src      └──────┘└────────────┘ └──────────────┘└───
typ      └──────┘└────────────┘ └──────────────┘└───
doc      └──────┘                               └───
txt      └──────┘                               └───
par      └──────┘                               └───
pid      └───┘└─┘                               └───
st   ────────────────────────────────────────────────
249        (int.cast_le.2 $ (hf n).2 _ ⟨y, yS, floor_le _⟩),
id          └─────────┘      └┘          └┘  └──────┘
src  ─────┘ └─────────┘└─┘     └────┘  └┘  └┘└──────┘└──┘
typ  ─────┘ └─────────┘└─┘  └┘└────┘ └┘└┘└┘└──────┘└──┘
doc  ─────┘            └─┘     └────┘  └┘  └┘        └──┘
txt  ─────┘            └─┘     └────┘  └┘  └┘        └──┘
par  ─────┘            └─┘     └────┘  └┘  └┘        └──┘
pid  ─────┘            └─┘     └────┘  └┘  └┘        └──┘
st   ─────────────────────────────────────────────────────┘└─
250      simp [-sub_eq_add_neg],
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid          └───────────────┘
st   ─────────────────────────┘└─
251      rwa [lt_div_iff ((nat.cast_pos.2 n0):((_:ℝ) < _)), sub_mul, _root_.inv_mul_cancel],
id            └────────┘   └──────────┘   └┘                └─────┘  └───────────────────┘
src      └───┘└────────┘  └──────────┘└─┘  └┘  └┘ └┘ └────┘└─────┘└┘└───────────────────┘
typ      └───┘└────────┘  └──────────┘└─┘└┘└┘  └┘ └┘ └────┘└─────┘└┘└───────────────────┘
doc      └───┘                        └─┘  └┘  └┘ └┘ └────┘       └┘                     
txt      └───┘                        └─┘  └┘  └┘ └┘ └────┘       └┘                     
par      └───┘                        └─┘  └┘  └┘ └┘ └────┘       └┘                     
pid         └┘                        └─┘  └┘  └┘ └┘ └────┘       └┘                     
st   ────────────────────────────────────────────────────┘└───────┘└─────────────────────┘└─
252      exact ne_of_gt (nat.cast_pos.2 n0) },
id             └──────┘  └──────────┘   └┘
src      └────┘└──────┘ └──────────┘└─┘  └┘
typ      └────┘└──────┘ └──────────┘└─┘└┘└┘
doc      └────┘                     └─┘  └┘
txt      └────┘                     └─┘  └┘
par      └────┘                     └─┘  └┘
pid                                └─┘  
st   ──────────────────────────────────────┘└┘
253    suffices hg, let g : cau_seq ℚ abs := ⟨λ n, f n / n, hg⟩,
id                          └─────┘   └─┘                  └┘
src    └─────────┘  └──────┘└─────┘ └─┘└──┘  └──┘    └┘  
typ    └─────────┘  └──────┘└─────┘ └─┘└──┘  └──┘   └┘└┘
doc    └─────────┘  └──────┘           └──┘  └──┘    └┘  
txt    └─────────┘  └──────┘           └──┘  └──┘    └┘  
par    └─────────┘  └──────┘           └──┘  └──┘    └┘  
pid    └─────────┘  └───┘└─┘           └──┘  └──┘    └┘  
st   ────────────┘└───────────────────────────────────────────┘└─
254    refine ⟨mk g, λ y, ⟨λ h x xS, le_trans _ h, λ h, _⟩⟩,
id             └┘                   └──────┘
src    └─────┘ └┘ └┘ └──┘  └───────┘└──────┘└─┘ └┘ └─────┘
typ    └─────┘ └┘└┘ └──┘  └───────┘└──────┘└─┘ └┘ └─────┘
doc    └─────┘    └┘ └──┘  └───────┘        └─┘ └┘ └─────┘
txt    └─────┘    └┘ └──┘  └───────┘        └─┘ └┘ └─────┘
par    └─────┘    └┘ └──┘  └───────┘        └─┘ └┘ └─────┘
pid              └┘ └──┘  └───────┘        └─┘ └┘ └─────┘
st   ─────────────────────────────────────────────────────┘└─
255    { refine le_of_forall_ge_of_dense (λ z xz, _),
id              └──────────────────────┘
src      └─────┘└──────────────────────┘  └───────┘
typ      └─────┘└──────────────────────┘  └───────┘
doc      └─────┘                          └───────┘
txt      └─────┘                          └───────┘
par      └─────┘                          └───────┘
pid                                      └───────┘
st   ───┘└─────────────────────────────────────────┘└─
256      cases exists_nat_gt (x - z)⁻¹ with K hK,
id             └───────────┘     
src      └────┘└───────────┘      └────────┘
typ      └────┘└───────────┘    └────────┘
doc      └────┘                   └────────┘
txt      └────┘                   └────────┘
par      └────┘                   └────────┘
pid                              └────────┘
st   ──────────────────────────────────────────┘└─
257      refine le_mk_of_forall_le ⟨K, λ n nK, _⟩,
id              └────────────────┘  
src      └─────┘└────────────────┘  └┘ └───────┘
typ      └─────┘└────────────────┘ └┘ └───────┘
doc      └─────┘                    └┘ └───────┘
txt      └─────┘                    └┘ └───────┘
par      └─────┘                    └┘ └───────┘
pid                                └┘ └───────┘
st   ───────────────────────────────────────────┘└─
258      replace xz := sub_pos.2 xz,
id                     └─────┘   └┘
src      └────────────┘└─────┘└─┘
typ      └────────────┘└─────┘└─┘└┘
doc      └────────────┘       └─┘
txt      └────────────┘       └─┘
par      └────────────┘       └─┘
pid             └─┘└─┘       └─┘
st   ─────────────────────────────┘└─
259      replace hK := le_trans (le_of_lt hK) (nat.cast_le.2 nK),
id                     └──────┘  └──────┘ └┘   └─────────┘   └┘
src      └────────────┘└──────┘ └──────┘  └┘ └─────────┘└─┘  
typ      └────────────┘└──────┘ └──────┘└┘└┘ └─────────┘└─┘└┘
doc      └────────────┘                   └┘            └─┘  
txt      └────────────┘                   └┘            └─┘  
par      └────────────┘                   └┘            └─┘  
pid             └─┘└─┘                   └┘            └─┘  
st   ──────────────────────────────────────────────────────────┘└─
260      have n0 : 0 < n := nat.cast_pos.1 (lt_of_lt_of_le (inv_pos xz) hK),
id                         └──────────┘    └────────────┘  └─────┘ └┘  └┘
src      └──────────┘  └──┘└──────────┘└─┘ └────────────┘ └─────┘  └┘  
typ      └──────────┘ └──┘└──────────┘└─┘ └────────────┘ └─────┘└┘└┘└┘
doc      └──────────┘  └──┘            └─┘                         └┘  
txt      └──────────┘  └──┘            └─┘                         └┘  
par      └──────────┘  └──┘            └─┘                         └┘  
pid      └─────┘└───┘  └──┘            └─┘                         └┘  
st   ─────────────────────────────────────────────────────────────────────┘└─
261      refine le_trans _ (le_of_lt $ hf₂ _ n0 _ xS),
id              └──────┘    └──────┘   └─┘   └┘   └┘
src      └─────┘└──────┘└─┘ └──────┘    └─┘  └─┘  
typ      └─────┘└──────┘└─┘ └──────┘ └─┘└─┘└┘└─┘└┘
doc      └─────┘        └─┘             └─┘  └─┘  
txt      └─────┘        └─┘             └─┘  └─┘  
par      └─────┘        └─┘             └─┘  └─┘  
pid                    └─┘             └─┘  └─┘  
st   ───────────────────────────────────────────────┘└─
262      rwa [le_sub, inv_le ((nat.cast_pos.2 n0):((_:ℝ) < _)) xz] },
id            └────┘  └────┘   └──────────┘   └┘               └┘
src      └───┘└────┘└┘└────┘  └──────────┘└─┘  └┘  └┘ └┘ └───┘  └┘
typ      └───┘└────┘└┘└────┘  └──────────┘└─┘└┘└┘  └┘ └┘ └───┘└┘└┘
doc      └───┘      └┘                    └─┘  └┘  └┘ └┘ └───┘  └┘
txt      └───┘      └┘                    └─┘  └┘  └┘ └┘ └───┘  └┘
par      └───┘      └┘                    └─┘  └┘  └┘ └┘ └───┘  └┘
pid         └┘      └┘                    └─┘  └┘  └┘ └┘ └───┘  
st   ──────────────┘└───────────────────────────────────────────┘└┘
263    { exact mk_le_of_forall_le ⟨1, λ n n1,
id             └────────────────┘
src      └────┘└────────────────┘ └─┘ └──────
typ      └────┘└────────────────┘ └─┘ └──────
doc      └────┘                   └─┘ └──────
txt      └────┘                   └─┘ └──────
par      └────┘                   └─┘ └──────
pid                              └─┘ └──────
st   ───┘└────────────────────────────────────
264        let ⟨x, xS, hx⟩ := hf₁ _ n1 in le_trans hx (h _ xS)⟩ },
id                 └┘  └┘     └─┘         └──────┘     
src  ─────┘     └┘  └┘  └───┘   └─┘  └──┘└──────┘    └─┘  └─┘
typ  ─────┘     └┘└┘└┘└┘└───┘└─┘└─┘  └──┘└──────┘   └─┘  └─┘
doc  ─────┘     └┘  └┘  └───┘   └─┘  └──┘            └─┘  └─┘
txt  ─────┘     └┘  └┘  └───┘   └─┘  └──┘            └─┘  └─┘
par  ─────┘     └┘  └┘  └───┘   └─┘  └──┘            └─┘  └─┘
pid  ─────┘     └┘  └┘  └───┘   └─┘  └──┘            └─┘  └┘
st   ──────────────────────────────────────────────────────────┘└┘
265    intros ε ε0,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
266    suffices : ∀ j k ≥ nat_ceil ε⁻¹, (f j / j - f k / k : ℚ) < ε,
id                        └──────┘                               
src    └─────────┘ └─────┘└──────┘              └─┘ └┘ 
typ    └─────────┘ └─────┘└──────┘             └─┘ └┘ 
doc    └─────────┘ └─────┘└──────┘              └─┘ └┘ 
txt    └─────────┘ └─────┘                      └─┘ └┘ 
par    └─────────┘ └─────┘                      └─┘ └┘ 
pid    └───────┘└┘ └─────┘                      └─┘ └┘ 
st   ─────────────────────────────────────────────────────────────┘└─
267    { refine ⟨_, λ j ij, abs_lt.2 ⟨_, this _ _ ij (le_refl _)⟩⟩,
id                          └────┘       └──┘         └─────┘
src      └─────┘ └─┘ └─────┘└────┘└─┘ └─┘    └───┘   └─────┘└───┘
typ      └─────┘ └─┘ └─────┘└────┘└─┘ └─┘└──┘└───┘   └─────┘└───┘
doc      └─────┘ └─┘ └─────┘      └─┘ └─┘    └───┘          └───┘
txt      └─────┘ └─┘ └─────┘      └─┘ └─┘    └───┘          └───┘
par      └─────┘ └─┘ └─────┘      └─┘ └─┘    └───┘          └───┘
pid             └─┘ └─────┘      └─┘ └─┘    └───┘          └───┘
st   ───┘└───────────────────────────────────────────────────────┘└─
268      rw [neg_lt, neg_sub], exact this _ _ (le_refl _) ij },
id           └────┘  └─────┘         └──┘      └─────┘    └┘
src      └──┘└────┘└┘└─────┘  └────┘    └───┘ └─────┘└──┘  
typ      └──┘└────┘└┘└─────┘  └────┘└──┘└───┘ └─────┘└──┘└┘
doc      └──┘      └┘         └────┘    └───┘        └──┘  
txt      └──┘      └┘         └────┘    └───┘        └──┘  
par      └──┘      └┘         └────┘    └───┘        └──┘  
pid        └┘      └┘                  └───┘        └──┘  
st   ─────────────┘└───────┘└───────────────────────────────┘└┘
269    intros j k ij ik,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
270    replace ij := le_trans (le_nat_ceil _) (nat.cast_le.2 ij),
id                   └──────┘  └─────────┘     └─────────┘   └┘
src    └────────────┘└──────┘ └─────────┘└──┘ └─────────┘└─┘  
typ    └────────────┘└──────┘ └─────────┘└──┘ └─────────┘└─┘└┘
doc    └────────────┘                    └──┘            └─┘  
txt    └────────────┘                    └──┘            └─┘  
par    └────────────┘                    └──┘            └─┘  
pid           └─┘└─┘                    └──┘            └─┘  
st   ──────────────────────────────────────────────────────────┘└─
271    replace ik := le_trans (le_nat_ceil _) (nat.cast_le.2 ik),
id                   └──────┘  └─────────┘     └─────────┘   └┘
src    └────────────┘└──────┘ └─────────┘└──┘ └─────────┘└─┘  
typ    └────────────┘└──────┘ └─────────┘└──┘ └─────────┘└─┘└┘
doc    └────────────┘                    └──┘            └─┘  
txt    └────────────┘                    └──┘            └─┘  
par    └────────────┘                    └──┘            └─┘  
pid           └─┘└─┘                    └──┘            └─┘  
st   ──────────────────────────────────────────────────────────┘└─
272    have j0 := nat.cast_pos.1 (lt_of_lt_of_le (inv_pos ε0) ij),
id                └──────────┘    └────────────┘  └─────┘ └┘  └┘
src    └─────────┘└──────────┘└─┘ └────────────┘ └─────┘  └┘  
typ    └─────────┘└──────────┘└─┘ └────────────┘ └─────┘└┘└┘└┘
doc    └─────────┘            └─┘                         └┘  
txt    └─────────┘            └─┘                         └┘  
par    └─────────┘            └─┘                         └┘  
pid    └─────┘└─┘            └─┘                         └┘  
st   ───────────────────────────────────────────────────────────┘└─
273    have k0 := nat.cast_pos.1 (lt_of_lt_of_le (inv_pos ε0) ik),
id                └──────────┘    └────────────┘  └─────┘ └┘  └┘
src    └─────────┘└──────────┘└─┘ └────────────┘ └─────┘  └┘  
typ    └─────────┘└──────────┘└─┘ └────────────┘ └─────┘└┘└┘└┘
doc    └─────────┘            └─┘                         └┘  
txt    └─────────┘            └─┘                         └┘  
par    └─────────┘            └─┘                         └┘  
pid    └─────┘└─┘            └─┘                         └┘  
st   ───────────────────────────────────────────────────────────┘└─
274    rcases hf₁ _ j0 with ⟨y, yS, hy⟩,
id            └─┘   └┘
src    └─────┘   └─┘  └───────────────┘
typ    └─────┘└─┘└─┘└┘└───────────────┘
doc    └─────┘   └─┘  └───────────────┘
txt    └─────┘   └─┘  └───────────────┘
par    └─────┘   └─┘  └───────────────┘
pid             └─┘  └───────────────┘
st   ─────────────────────────────────┘└─
275    refine lt_of_lt_of_le ((@rat.cast_lt ℝ _ _ _).1 _)
id            └────────────┘    └─────────┘
src    └─────┘└────────────┘   └─────────┘ └────────────
typ    └─────┘└────────────┘   └─────────┘ └────────────
doc    └─────┘                             └────────────
txt    └─────┘                             └────────────
par    └─────┘                             └────────────
pid                                       └────────────
st   ─────────────────────────────────────────────────────
276      ((inv_le ε0 (nat.cast_pos.2 k0)).1 ik),
id         └────┘ └┘  └──────────┘   └┘     └┘
src  ───┘  └────┘   └──────────┘└─┘  └───┘  
typ  ───┘  └────┘└┘ └──────────┘└─┘└┘└───┘└┘
doc  ───┘                       └─┘  └───┘  
txt  ───┘                       └─┘  └───┘  
par  ───┘                       └─┘  └───┘  
pid  ───┘                       └─┘  └───┘  
st   ─────────────────────────────────────────┘└─
277    simpa using sub_lt_iff_lt_add'.2
id                 └────────────────┘
src    └──────────┘└────────────────┘└──
typ    └──────────┘└────────────────┘└──
doc    └──────────┘                  └──
txt    └──────────┘                  └──
par    └──────────┘                  └──
pid         └────┘                  └──
st   ───────────────────────────────────
278      (lt_of_le_of_lt hy $ sub_lt_iff_lt_add.1 $ hf₂ _ k0 _ yS)
id        └────────────┘ └┘   └───────────────┘     └─┘   └┘   └┘
src  ───┘ └────────────┘   └───────────────┘└─┘    └─┘  └─┘  └┘
typ  ───┘ └────────────┘└┘ └───────────────┘└─┘ └─┘└─┘└┘└─┘└┘└┘
doc  ───┘                                   └─┘    └─┘  └─┘  └┘
txt  ───┘                                   └─┘    └─┘  └─┘  └┘
par  ───┘                                   └─┘    └─┘  └─┘  └┘
pid  ───┘                                   └─┘    └─┘  └─┘  
st   ─────────────────────────────────────────────────────────────┘
279  end
st   └─┘
280  
281  noncomputable def Sup (S : set ℝ) : ℝ :=
id                              └─┘     
src                             └─┘     
typ                             └─┘     
282  if h : (∃ x, x ∈ S) ∧ (∃ x, ∀ y ∈ S, y ≤ x)
id   └┘                         
src  └┘                               
typ  └┘                         
283  then classical.some (exists_sup S h.1 h.2) else 0
id        └────────────┘  └────────┘            
src       └────────────┘  └────────┘               
typ       └────────────┘  └────────┘            
284  
285  theorem Sup_le (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x)
id                       └─┘                                
src                      └─┘                                      
typ                      └─┘                                
286    {y} : Sup S ≤ y ↔ ∀ z ∈ S, z ≤ y :=
id           └─┘              
src          └─┘                  
typ          └─┘              
287  by simp [Sup, h₁, h₂]; exact
id            └─┘  └┘  └┘
src     └────┘└─┘└┘  └┘    └────┘
typ     └────┘└─┘└┘└┘└┘└┘  └────┘
doc     └────┘   └┘  └┘    └────┘
txt     └────┘   └┘  └┘    └────┘
par     └────┘   └┘  └┘    └────┘
pid            └┘  └┘         
st     └──────────────────────────
288  classical.some_spec (exists_sup S h₁ h₂) y
id   └─────────────────┘  └────────┘  └┘ └┘  
src  └─────────────────┘ └────────┘     └┘ 
typ  └─────────────────┘ └────────┘└┘└┘└┘
doc                                     └┘ 
txt                                     └┘ 
par                                     └┘ 
pid                                     └┘ 
st   ───────────────────────────────────────────
289  
src  
typ  
doc  
txt  
par  
pid  
st   
290  section
291  -- this proof times out without this
292  local attribute [instance, priority 1000] classical.prop_decidable
id                                             └──────────────────────┘
src                                            └──────────────────────┘
typ                                            └──────────────────────┘
293  theorem lt_Sup (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x)
id                       └─┘                                
src                      └─┘                                      
typ                      └─┘                                
294    {y} : y < Sup S ↔ ∃ z ∈ S, y < z :=
id             └─┘          
src             └─┘             
typ            └─┘          
295  by simpa [not_forall] using not_congr (@Sup_le S h₁ h₂ y)
id             └────────┘        └───────┘   └────┘  └┘ └┘ 
src     └─────┘└────────┘└──────┘└───────┘  └────┘      └┘
typ     └─────┘└────────┘└──────┘└───────┘  └────┘└┘└┘└┘
doc     └─────┘          └──────┘                       └┘
txt     └─────┘          └──────┘                       └┘
par     └─────┘          └──────┘                       └┘
pid                    └────┘                       
st     └──────────────────────────────────────────────────────┘
296  end
297  
298  theorem le_Sup (S : set ℝ) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x) {x} (xS : x ∈ S) : x ≤ Sup S :=
id                       └─┘                                        └─┘ 
src                      └─┘                                                └─┘
typ                      └─┘                                        └─┘ 
299  (Sup_le S ⟨_, xS⟩ h₂).1 (le_refl _) _ xS
id    └────┘      └┘  └┘    └─────┘      └┘
src   └────┘                 └─────┘
typ   └────┘      └┘  └┘    └─────┘      └┘
300  
301  theorem Sup_le_ub (S : set ℝ) (h₁ : ∃ x, x ∈ S) {ub} (h₂ : ∀ y ∈ S, y ≤ ub) : Sup S ≤ ub :=
id                          └─┘                                   └┘    └─┘   └┘
src                         └─┘                                               └─┘   
typ                         └─┘                                   └┘    └─┘   └┘
302  (Sup_le S h₁ ⟨_, h₂⟩).2 h₂
id    └────┘  └┘     └┘    └┘
src   └────┘              
typ   └────┘  └┘     └┘    └┘
303  
304  protected lemma is_lub_Sup {s : set ℝ} {a b : ℝ} (ha : a ∈ s) (hb : b ∈ upper_bounds s) :
id                                   └─┘                              └──────────┘ 
src                                  └─┘                                 └──────────┘
typ                                  └─┘                              └──────────┘ 
doc                                                                          └──────────┘
305    is_lub s (Sup s) :=
id     └────┘   └─┘ 
src    └────┘    └─┘
typ    └────┘   └─┘ 
doc    └────┘
306  ⟨λ x xs, real.le_Sup s ⟨_, hb⟩ xs,
id       └┘  └─────────┘      └┘  └┘
src           └─────────┘
typ      └┘  └─────────┘      └┘  └┘
307   λ u h, real.Sup_le_ub _ ⟨_, ha⟩ h⟩
id         └────────────┘       └┘  
src          └────────────┘
typ        └────────────┘       └┘  
308  
309  noncomputable def Inf (S : set ℝ) : ℝ := -Sup {x | -x ∈ S}
id                              └─┘         └─┘      
src                             └─┘         └─┘       
typ                             └─┘         └─┘      
310  
311  theorem le_Inf (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, x ≤ y)
id                       └─┘                                
src                      └─┘                                      
typ                      └─┘                                
312    {y} : y ≤ Inf S ↔ ∀ z ∈ S, y ≤ z :=
id             └─┘            
src             └─┘               
typ            └─┘            
313  begin
st   └─────
314    refine le_neg.trans ((Sup_le _ _ _).trans _),
id            └──────────┘   └────┘
src    └─────┘└──────────┘  └────┘└──────────────┘
typ    └─────┘└──────────┘  └────┘└──────────────┘
doc    └─────┘                    └──────────────┘
txt    └─────┘                    └──────────────┘
par    └─────┘                    └──────────────┘
pid                              └──────────────┘
st   ─────────────────────────────────────────────┘└─
315    { cases h₁ with x xS, exact ⟨-x, by simp [xS]⟩ },
id             └┘                              └┘
src      └────┘  └────────┘  └────┘  └┘  └────┘  └┘
typ      └────┘└┘└────────┘  └────┘ └┘  └────┘└┘└┘
doc      └────┘  └────────┘  └────┘   └┘  └────┘  └┘
txt      └────┘  └────────┘  └────┘   └┘  └────┘  └┘
par      └────┘  └────────┘  └────┘   └┘  └────┘  └┘
pid             └────────┘          └┘  └─────┘  └┘
st   ───┘└────────────────┘└─────────────┘└────────┘└┘└┘
316    { cases h₂ with ub h, exact ⟨-ub, λ y hy, le_neg.1 $ h _ hy⟩ },
id             └┘                    └┘          └────┘     
src      └────┘  └────────┘  └────┘    └┘ └─────┘└────┘└─┘  └─┘  └┘
typ      └────┘└┘└────────┘  └────┘  └┘└┘ └─────┘└────┘└─┘ └─┘  └┘
doc      └────┘  └────────┘  └────┘    └┘ └─────┘      └─┘  └─┘  └┘
txt      └────┘  └────────┘  └────┘    └┘ └─────┘      └─┘  └─┘  └┘
par      └────┘  └────────┘  └────┘    └┘ └─────┘      └─┘  └─┘  └┘
pid             └────────┘           └┘ └─────┘      └─┘  └─┘  
st   ───┘└────────────────┘└───────────────────────────────────────┘└┘
317    split; intros H z hz,
src    └───┘  └───────────┘
typ    └───┘  └───────────┘
doc    └───┘  └───────────┘
txt    └───┘  └───────────┘
par    └───┘  └───────────┘
pid                 └─────┘
st   ─────────────────────┘└─
318    { exact neg_le_neg_iff.1 (H _ $ by simp [hz]) },
id             └────────────┘                  └┘
src      └────┘└────────────┘└─┘  └─┘   └────┘  └┘
typ      └────┘└────────────┘└─┘ └─┘   └────┘└┘└┘
doc      └────┘              └─┘  └─┘   └────┘  └┘
txt      └────┘              └─┘  └─┘   └────┘  └┘
par      └────┘              └─┘  └─┘   └────┘  └┘
pid                         └─┘  └─┘   └─────┘  └┘
st   ───┘└──────────────────────────────┘└────────┘└┘└┘
319    { exact le_neg.2 (H _ hz) }
id             └────┘       └┘
src      └────┘└────┘└─┘  └─┘  └┘
typ      └────┘└────┘└─┘ └─┘└┘└┘
doc      └────┘      └─┘  └─┘  └┘
txt      └────┘      └─┘  └─┘  └┘
par      └────┘      └─┘  └─┘  └┘
pid                 └─┘  └─┘  
st   ───────────────────────────┘└─
320  end
st   ──┘
321  
322  section
323  -- this proof times out without this
324  local attribute [instance, priority 1000] classical.prop_decidable
id                                             └──────────────────────┘
src                                            └──────────────────────┘
typ                                            └──────────────────────┘
325  theorem Inf_lt (S : set ℝ) (h₁ : ∃ x, x ∈ S) (h₂ : ∃ x, ∀ y ∈ S, x ≤ y)
id                       └─┘                                
src                      └─┘                                      
typ                      └─┘                                
326    {y} : Inf S < y ↔ ∃ z ∈ S, z < y :=
id           └─┘            
src          └─┘                
typ          └─┘            
327  by simpa [not_forall] using not_congr (@le_Inf S h₁ h₂ y)
id             └────────┘        └───────┘   └────┘  └┘ └┘ 
src     └─────┘└────────┘└──────┘└───────┘  └────┘      └┘
typ     └─────┘└────────┘└──────┘└───────┘  └────┘└┘└┘└┘
doc     └─────┘          └──────┘                       └┘
txt     └─────┘          └──────┘                       └┘
par     └─────┘          └──────┘                       └┘
pid                    └────┘                       
st     └──────────────────────────────────────────────────────┘
328  end
329  
330  theorem Inf_le (S : set ℝ) (h₂ : ∃ x, ∀ y ∈ S, x ≤ y) {x} (xS : x ∈ S) : Inf S ≤ x :=
id                       └─┘                                      └─┘   
src                      └─┘                                             └─┘   
typ                      └─┘                                      └─┘   
331  (le_Inf S ⟨_, xS⟩ h₂).1 (le_refl _) _ xS
id    └────┘      └┘  └┘    └─────┘      └┘
src   └────┘                 └─────┘
typ   └────┘      └┘  └┘    └─────┘      └┘
332  
333  theorem lb_le_Inf (S : set ℝ) (h₁ : ∃ x, x ∈ S) {lb} (h₂ : ∀ y ∈ S, lb ≤ y) : lb ≤ Inf S :=
id                          └─┘                                 └┘      └┘  └─┘ 
src                         └─┘                                                   └─┘
typ                         └─┘                                 └┘      └┘  └─┘ 
334  (le_Inf S h₁ ⟨_, h₂⟩).2 h₂
id    └────┘  └┘     └┘    └┘
src   └────┘              
typ   └────┘  └┘     └┘    └┘
335  
336  open lattice
337  noncomputable instance lattice : lattice ℝ := by apply_instance
id                                    └─────┘ 
src                                   └─────┘        └──────────────
typ                                   └─────┘        └──────────────
doc                                   └─────┘         └──────────────
txt                                                   └──────────────
par                                                   └──────────────
pid                                                                 
st                                                   └───────────────
338  
src  
typ  
doc  
txt  
par  
pid  
st   
339  noncomputable instance : conditionally_complete_linear_order ℝ :=
id                            └─────────────────────────────────┘ 
src                           └─────────────────────────────────┘ 
typ                           └─────────────────────────────────┘ 
340  { Sup := real.Sup,
id            └──────┘
src           └──────┘
typ           └──────┘
341    Inf := real.Inf,
id            └──────┘
src           └──────┘
typ           └──────┘
342    le_cSup :=
343      assume (s : set ℝ) (a : ℝ) (_ : bdd_above s) (_ : a ∈ s),
id                   └─┘               └───────┘          
src                  └─┘               └───────┘           
typ                  └─┘               └───────┘          
doc                                      └───────┘
344      show a ≤ Sup s,
id              └─┘ 
src              └─┘
typ             └─┘ 
345        from le_Sup s ‹bdd_above s› ‹a ∈ s›,
id              └────┘  └───────┘    
src             └────┘   └───────┘       
typ             └────┘  └───────┘    
doc                      └───────┘        
346    cSup_le :=
347      assume (s : set ℝ) (a : ℝ) (_ : s.nonempty) (H : ∀b∈s, b ≤ a),
id                   └─┘               └───────┘             
src                  └─┘                └───────┘               
typ                  └─┘               └───────┘             
doc                                       └───────┘
348      show Sup s ≤ a,
id            └─┘   
src           └─┘   
typ           └─┘   
349        from Sup_le_ub s ‹s.nonempty› H,
id              └───────┘  └───────┘ 
src             └───────┘    └───────┘
typ             └───────┘  └───────┘ 
doc                          └───────┘
350    cInf_le :=
351      assume (s : set ℝ) (a : ℝ) (_ : bdd_below s) (_ : a ∈ s),
id                   └─┘               └───────┘          
src                  └─┘               └───────┘           
typ                  └─┘               └───────┘          
doc                                      └───────┘
352      show Inf s ≤ a,
id            └─┘   
src           └─┘   
typ           └─┘   
353        from Inf_le s ‹bdd_below s› ‹a ∈ s›,
id              └────┘  └───────┘    
src             └────┘   └───────┘       
typ             └────┘  └───────┘    
doc                      └───────┘        
354    le_cInf :=
355      assume (s : set ℝ) (a : ℝ) (_ : s.nonempty) (H : ∀b∈s, a ≤ b),
id                   └─┘               └───────┘             
src                  └─┘                └───────┘               
typ                  └─┘               └───────┘             
doc                                       └───────┘
356      show a ≤ Inf s,
id              └─┘ 
src              └─┘
typ             └─┘ 
357        from lb_le_Inf s ‹s.nonempty› H,
id              └───────┘  └───────┘ 
src             └───────┘    └───────┘
typ             └───────┘  └───────┘ 
doc                          └───────┘
358    decidable_le := classical.dec_rel _,
id                     └───────────────┘
src                    └───────────────┘
typ                    └───────────────┘
359   ..real.linear_order, ..real.lattice}
id      └───────────────┘    └──────────┘
src     └───────────────┘    └──────────┘
typ     └───────────────┘    └──────────┘
360  
361  theorem Sup_empty : lattice.Sup (∅ : set ℝ) = 0 := dif_neg $ by simp
id                       └─────────┘     └─┘         └─────┘
src                      └─────────┘     └─┘         └─────┘      └────
typ                      └─────────┘     └─┘         └─────┘      └────
doc                      └─────────┘                                 └────
txt                                                                  └────
par                                                                  └────
pid                                                                      
st                                                                  └─────
362  
src  
typ  
doc  
txt  
par  
pid  
st   
363  theorem Sup_of_not_bdd_above {s : set ℝ} (hs : ¬ bdd_above s) : lattice.Sup s = 0 :=
id                                     └─┘          └───────┘     └─────────┘  
src                                    └─┘          └───────┘      └─────────┘   
typ                                    └─┘          └───────┘     └─────────┘  
doc                                                   └───────┘      └─────────┘
364  dif_neg $ assume h, hs h.2
id   └─────┘            └┘ 
src  └─────┘                 
typ  └─────┘            └┘ 
365  
366  theorem Sup_univ : real.Sup set.univ = 0 :=
id                      └──────┘ └──────┘ 
src                     └──────┘ └──────┘ 
typ                     └──────┘ └──────┘ 
367  real.Sup_of_not_bdd_above $ λ ⟨x, h⟩, not_le_of_lt (lt_add_one _) $ h (set.mem_univ _)
id   └───────────────────────┘           └──────────┘  └────────┘         └──────────┘
src  └───────────────────────┘             └──────────┘  └────────┘         └──────────┘
typ  └───────────────────────┘           └──────────┘  └────────┘         └──────────┘
368  
369  theorem Inf_empty : lattice.Inf (∅ : set ℝ) = 0 :=
id                       └─────────┘     └─┘   
src                      └─────────┘     └─┘   
typ                      └─────────┘     └─┘   
doc                      └─────────┘
370  show Inf ∅ = 0, by simp [Inf]; exact Sup_empty
id        └─┘               └─┘         └───────┘
src       └─┘         └────┘└─┘  └────┘└───────┘
typ       └─┘         └────┘└─┘  └────┘└───────┘
doc                     └────┘     └────┘         
txt                     └────┘     └────┘         
par                     └────┘     └────┘         
pid                                            
st                     └────────────────────────────
371  
src  
typ  
doc  
txt  
par  
pid  
st   
372  theorem Inf_of_not_bdd_below {s : set ℝ} (hs : ¬ bdd_below s) : lattice.Inf s = 0 :=
id                                     └─┘          └───────┘     └─────────┘  
src                                    └─┘          └───────┘      └─────────┘   
typ                                    └─┘          └───────┘     └─────────┘  
doc                                                   └───────┘      └─────────┘
373  have bdd_above {x | -x ∈ s} → bdd_below s, from
id        └───────┘          └───────┘ 
src       └───────┘             └───────┘
typ       └───────┘          └───────┘ 
doc       └───────┘                └───────┘
374    assume ⟨b, hb⟩, ⟨-b, assume x hxs, neg_le.2 $ hb $ by simp [hxs]⟩,
id              └┘               └─┘  └────┘                  └─┘
src                                      └────┘            └────┘   
typ             └┘               └─┘  └────┘            └────┘└─┘
doc                                                          └────┘   
txt                                                          └────┘   
par                                                          └────┘   
pid                                                                 
st                                                          └─────────┘
375  have ¬ bdd_above {x | -x ∈ s}, from mt this hs,
id         └───────┘              └┘ └──┘ └┘
src        └───────┘                 └┘
typ        └───────┘              └┘ └──┘ └┘
doc         └───────┘
376  neg_eq_zero.2 $ Sup_of_not_bdd_above $ this
id   └─────────┘    └──────────────────┘   └──┘
src  └─────────┘    └──────────────────┘
typ  └─────────┘    └──────────────────┘   └──┘
377  
378  theorem cau_seq_converges (f : cau_seq ℝ abs) : ∃ x, f ≈ const abs x :=
id                                  └─────┘  └─┘        └───┘ └─┘ 
src                                 └─────┘  └─┘          └───┘ └─┘
typ                                 └─────┘  └─┘        └───┘ └─┘ 
doc                                                           └───┘
379  begin
st   └─────
380    let S := {x : ℝ | const abs x < f},
id                      └───┘ └─┘    
src    └───────┘└──┘ └─┘└───┘└─┘  
typ    └───────┘└──┘ └─┘└───┘└─┘ 
doc    └───────┘ └──┘ └─┘└───┘      
txt    └───────┘ └──┘ └─┘           
par    └───────┘ └──┘ └─┘           
pid    └───┘└─┘ └──┘ └─┘           
st   ───────────────────────────────────┘└─
381    have lb : ∃ x, x ∈ S := exists_lt f,
id                         └───────┘ 
src    └────────┘└┘  └──┘└───────┘
typ    └────────┘└┘ └──┘└───────┘
doc    └────────┘ └┘    └──┘         
txt    └────────┘ └┘    └──┘         
par    └────────┘ └┘    └──┘         
pid    └─────┘└─┘ └┘    └──┘         
st   ────────────────────────────────────┘└─
382    have ub' : ∀ x, f < const abs x → ∀ y ∈ S, y ≤ x :=
id                       └───┘ └─┘               
src    └─────────┘ └┘   └───┘└─┘   └───┘    └───
typ    └─────────┘ └┘ └───┘└─┘   └───┘   └───
doc    └─────────┘ └┘   └───┘      └───┘     └───
txt    └─────────┘ └┘              └───┘     └───
par    └─────────┘ └┘              └───┘     └───
pid    └──────┘└─┘ └┘              └───┘     └───
st   ──────────────────────────────────────────────────────
383      λ x h y yS, le_of_lt $ const_lt.1 $ cau_seq.lt_trans yS h,
id                   └──────┘   └──────┘     └──────────────┘
src  ───┘ └─────────┘└──────┘ └──────┘└─┘ └──────────────┘  
typ  ───┘ └─────────┘└──────┘ └──────┘└─┘ └──────────────┘  
doc  ───┘ └─────────┘                 └─┘                   
txt  ───┘ └─────────┘                 └─┘                   
par  ───┘ └─────────┘                 └─┘                   
pid  ───┘ └─────────┘                 └─┘                   
st   ────────────────────────────────────────────────────────────┘└─
384    have ub : ∃ x, ∀ y ∈ S, y ≤ x := (exists_gt f).imp ub',
id                                    └───────┘       └─┘
src    └────────┘└┘ └───┘     └──┘ └───────┘ └────┘
typ    └────────┘└┘ └───┘    └──┘ └───────┘└────┘└─┘
doc    └────────┘ └┘  └───┘     └──┘           └────┘
txt    └────────┘ └┘  └───┘     └──┘           └────┘
par    └────────┘ └┘  └───┘     └──┘           └────┘
pid    └─────┘└─┘ └┘  └───┘     └──┘           └────┘
st   ───────────────────────────────────────────────────────┘└─
385    refine ⟨Sup S,
id             └─┘ 
src    └─────┘ └─┘ └─
typ    └─────┘ └─┘└─
doc    └─────┘     └─
txt    └─────┘     └─
par    └─────┘     └─
pid               └─
st   ─────────────────
386      ((lt_total _ _).resolve_left (λ h, _)).resolve_right (λ h, _)⟩,
id         └──────┘
src  ───┘  └──────┘└─────────────────┘  └────────────────────┘  └─────┘
typ  ───┘  └──────┘└─────────────────┘  └────────────────────┘  └─────┘
doc  ───┘          └─────────────────┘  └────────────────────┘  └─────┘
txt  ───┘          └─────────────────┘  └────────────────────┘  └─────┘
par  ───┘          └─────────────────┘  └────────────────────┘  └─────┘
pid  ───┘          └─────────────────┘  └────────────────────┘  └─────┘
st   ─────────────────────────────────────────────────────────────────┘└─
387    { rcases h with ⟨ε, ε0, i, ih⟩,
id              
src      └─────┘ └──────────────────┘
typ      └─────┘└──────────────────┘
doc      └─────┘ └──────────────────┘
txt      └─────┘ └──────────────────┘
par      └─────┘ └──────────────────┘
pid             └──────────────────┘
st   ───┘└──────────────────────────┘└─
388      refine not_lt_of_le (Sup_le_ub S lb (ub' _ _))
id              └──────────┘  └───────┘  └┘  └─┘
src      └─────┘└──────────┘ └───────┘       └──────
typ      └─────┘└──────────┘ └───────┘└┘ └─┘└──────
doc      └─────┘                             └──────
txt      └─────┘                             └──────
par      └─────┘                             └──────
pid                                         └──────
st   ───────────────────────────────────────────────────
389        ((sub_lt_self_iff _).2 (half_pos ε0)),
id           └─────────────┘       └──────┘ └┘
src  ─────┘  └─────────────┘└────┘ └──────┘  └┘
typ  ─────┘  └─────────────┘└────┘ └──────┘└┘└┘
doc  ─────┘                 └────┘           └┘
txt  ─────┘                 └────┘           └┘
par  ─────┘                 └────┘           └┘
pid  ─────┘                 └────┘           └┘
st   ──────────────────────────────────────────┘└─
390      refine ⟨_, half_pos ε0, i, λ j ij, _⟩,
id                  └──────┘ └┘  
src      └─────┘ └─┘└──────┘  └┘ └┘ └───────┘
typ      └─────┘ └─┘└──────┘└┘└┘└┘ └───────┘
doc      └─────┘ └─┘          └┘ └┘ └───────┘
txt      └─────┘ └─┘          └┘ └┘ └───────┘
par      └─────┘ └─┘          └┘ └┘ └───────┘
pid             └─┘          └┘ └┘ └───────┘
st   ────────────────────────────────────────┘└─
391      rw [sub_apply, const_apply, sub_right_comm,
id           └───────┘  └─────────┘  └────────────┘
src      └──┘└───────┘└┘└─────────┘└┘└────────────┘└─
typ      └──┘└───────┘└┘└─────────┘└┘└────────────┘└─
doc      └──┘         └┘           └┘              └─
txt      └──┘         └┘           └┘              └─
par      └──┘         └┘           └┘              └─
pid        └┘         └┘           └┘              └─
st   ────────────────┘└───────────┘└──────────────┘└─
392        le_sub_iff_add_le, add_halves],
id         └───────────────┘  └────────┘
src  ─────┘└───────────────┘└┘└────────┘
typ  ─────┘└───────────────┘└┘└────────┘
doc  ─────┘                 └┘          
txt  ─────┘                 └┘          
par  ─────┘                 └┘          
pid  ─────┘                 └┘          
st   ──────────────────────┘└──────────┘└──
393      exact ih _ ij },
id             └┘   └┘
src      └────┘  └─┘  
typ      └────┘└┘└─┘└┘
doc      └────┘  └─┘  
txt      └────┘  └─┘  
par      └────┘  └─┘  
pid             └─┘  
st   ─────────────────┘└┘
394    { rcases h with ⟨ε, ε0, i, ih⟩,
id              
src      └─────┘ └──────────────────┘
typ      └─────┘└──────────────────┘
doc      └─────┘ └──────────────────┘
txt      └─────┘ └──────────────────┘
par      └─────┘ └──────────────────┘
pid             └──────────────────┘
st   ───────────────────────────────┘└─
395      refine not_lt_of_le (le_Sup S ub _)
id              └──────────┘  └────┘  └┘
src      └─────┘└──────────┘ └────┘   └───
typ      └─────┘└──────────┘ └────┘└┘└───
doc      └─────┘                      └───
txt      └─────┘                      └───
par      └─────┘                      └───
pid                                  └───
st   ────────────────────────────────────────
396        ((lt_add_iff_pos_left _).2 (half_pos ε0)),
id           └─────────────────┘       └──────┘ └┘
src  ─────┘  └─────────────────┘└────┘ └──────┘  └┘
typ  ─────┘  └─────────────────┘└────┘ └──────┘└┘└┘
doc  ─────┘                     └────┘           └┘
txt  ─────┘                     └────┘           └┘
par  ─────┘                     └────┘           └┘
pid  ─────┘                     └────┘           └┘
st   ──────────────────────────────────────────────┘└─
397      refine ⟨_, half_pos ε0, i, λ j ij, _⟩,
id                  └──────┘ └┘  
src      └─────┘ └─┘└──────┘  └┘ └┘ └───────┘
typ      └─────┘ └─┘└──────┘└┘└┘└┘ └───────┘
doc      └─────┘ └─┘          └┘ └┘ └───────┘
txt      └─────┘ └─┘          └┘ └┘ └───────┘
par      └─────┘ └─┘          └┘ └┘ └───────┘
pid             └─┘          └┘ └┘ └───────┘
st   ────────────────────────────────────────┘└─
398      rw [sub_apply, const_apply, add_comm, ← sub_sub,
id           └───────┘  └─────────┘  └──────┘    └─────┘
src      └──┘└───────┘└┘└─────────┘└┘└──────┘└──┘└─────┘└─
typ      └──┘└───────┘└┘└─────────┘└┘└──────┘└──┘└─────┘└─
doc      └──┘         └┘           └┘        └──┘       └─
txt      └──┘         └┘           └┘        └──┘       └─
par      └──┘         └┘           └┘        └──┘       └─
pid        └┘         └┘           └┘        └──┘       └─
st   ────────────────┘└───────────┘└────────┘└─────────┘└─
399        le_sub_iff_add_le, add_halves],
id         └───────────────┘  └────────┘
src  ─────┘└───────────────┘└┘└────────┘
typ  ─────┘└───────────────┘└┘└────────┘
doc  ─────┘                 └┘          
txt  ─────┘                 └┘          
par  ─────┘                 └┘          
pid  ─────┘                 └┘          
st   ──────────────────────┘└──────────┘└──
400      exact ih _ ij }
id             └┘   └┘
src      └────┘  └─┘  
typ      └────┘└┘└─┘└┘
doc      └────┘  └─┘  
txt      └────┘  └─┘  
par      └────┘  └─┘  
pid             └─┘  
st   ─────────────────┘└─
401  end
st   ──┘
402  
403  noncomputable instance : cau_seq.is_complete ℝ abs := ⟨cau_seq_converges⟩
id                            └─────────────────┘  └─┘     └───────────────┘
src                           └─────────────────┘  └─┘     └───────────────┘
typ                           └─────────────────┘  └─┘     └───────────────┘
404  
405  theorem sqrt_exists : ∀ {x : ℝ}, 0 ≤ x → ∃ y, 0 ≤ y ∧ y * y = x :=
id                                                    
src                                                       
typ                                                   
406  suffices H : ∀ {x : ℝ}, 0 < x → x ≤ 1 → ∃ y, 0 < y ∧ y * y = x, begin
id                                                 
src                                                     
typ                                                
st                                                                   └─────
407    intros x x0, cases x0,
id                        └┘
src    └─────────┘  └────┘
typ    └─────────┘  └────┘└┘
doc    └─────────┘  └────┘
txt    └─────────┘  └────┘
par    └─────────┘  └────┘
pid          └───┘       
st   ────────────┘└────────┘└─
408    cases le_total x 1 with x1 x1,
id           └──────┘ 
src    └────┘└──────┘ └───────────┘
typ    └────┘└──────┘└───────────┘
doc    └────┘         └───────────┘
txt    └────┘         └───────────┘
par    └────┘         └───────────┘
pid                  └──────────┘
st   ──────────────────────────────┘└─
409    { rcases H x0 x1 with ⟨y, y0, hy⟩,
id               └┘ └┘
src      └─────┘     └───────────────┘
typ      └─────┘└┘└┘└───────────────┘
doc      └─────┘     └───────────────┘
txt      └─────┘     └───────────────┘
par      └─────┘     └───────────────┘
pid                 └───────────────┘
st   ───┘└─────────────────────────────┘└─
410      exact ⟨y, le_of_lt y0, hy⟩ },
id                └──────┘ └┘  └┘
src      └────┘  └┘└──────┘  └┘  └┘
typ      └────┘ └┘└──────┘└┘└┘└┘└┘
doc      └────┘  └┘          └┘  └┘
txt      └────┘  └┘          └┘  └┘
par      └────┘  └┘          └┘  └┘
pid             └┘          └┘  
st   ──────────────────────────────┘└┘
411    { have := (inv_le_inv x0 zero_lt_one).2 x1,
id                └────────┘ └┘ └─────────┘    └┘
src      └──────┘ └────────┘  └─────────┘└──┘
typ      └──────┘ └────────┘└┘└─────────┘└──┘└┘
doc      └──────┘                        └──┘
txt      └──────┘                        └──┘
par      └──────┘                        └──┘
pid      └───┘└─┘                        └──┘
st   ───┘└──────────────────────────────────────┘└─
412      rw inv_one at this,
id          └─────┘
src      └─┘└─────┘└──────┘
typ      └─┘└─────┘└──────┘
doc      └─┘       └──────┘
txt      └─┘       └──────┘
par      └─┘       └──────┘
pid               └──────┘
st   ─────────────────────┘└─
413      rcases H (inv_pos x0) this with ⟨y, y0, hy⟩,
id                └─────┘ └┘  └──┘
src      └─────┘  └─────┘  └┘    └───────────────┘
typ      └─────┘ └─────┘└┘└┘└──┘└───────────────┘
doc      └─────┘           └┘    └───────────────┘
txt      └─────┘           └┘    └───────────────┘
par      └─────┘           └┘    └───────────────┘
pid                       └┘    └───────────────┘
st   ──────────────────────────────────────────────┘└─
414      refine ⟨y⁻¹, le_of_lt (inv_pos y0), _⟩, rw [← mul_inv', hy, inv_inv'] },
id               └┘  └──────┘  └─────┘ └┘             └──────┘  └┘  └──────┘
src      └─────┘  └┘└┘└──────┘ └─────┘  └───┘  └────┘└──────┘└┘  └┘└──────┘└┘
typ      └─────┘ └┘└┘└──────┘ └─────┘└┘└───┘  └────┘└──────┘└┘└┘└┘└──────┘└┘
doc      └─────┘    └┘                  └───┘  └────┘        └┘  └┘        └┘
txt      └─────┘    └┘                  └───┘  └────┘        └┘  └┘        └┘
par      └─────┘    └┘                  └───┘  └────┘        └┘  └┘        └┘
pid                └┘                  └───┘    └──┘        └┘  └┘        
st   ─────────────────────────────────────────┘└──────────────┘└──┘└────────┘└┘
415    { exact ⟨0, by simp [x0.symm]⟩ }
src      └────┘ └─┘  └────┘       └┘
typ      └────┘ └─┘  └────┘└─────┘└┘
doc      └────┘ └─┘  └────┘       └┘
txt      └────┘ └─┘  └────┘       └┘
par      └────┘ └─┘  └────┘       └┘
pid            └─┘  └─────┘       └┘
st   ───────────────┘└─────────────┘└┘└─
416  end,
st   ──┘
417  λ x x0 x1, begin
id      └┘ └┘
typ     └┘ └┘
st              └─────
418    let S := {y | 0 < y ∧ y * y ≤ x},
id                               
src    └───────┘└────┘     
typ    └───────┘└────┘    
doc    └───────┘ └────┘        
txt    └───────┘ └────┘        
par    └───────┘ └────┘        
pid    └───┘└─┘ └────┘        
st   ─────────────────────────────────┘└─
419    have lb : x ∈ S := ⟨x0, by simpa using (mul_le_mul_right x0).2 x1⟩,
id                      └┘                  └──────────────┘ └┘    └┘
src    └────────┘  └──┘   └┘  └──────────┘ └──────────────┘  └──┘  
typ    └────────┘└──┘ └┘└┘  └──────────┘ └──────────────┘└┘└──┘└┘
doc    └────────┘   └──┘   └┘  └──────────┘                   └──┘  
txt    └────────┘   └──┘   └┘  └──────────┘                   └──┘  
par    └────────┘   └──┘   └┘  └──────────┘                   └──┘  
pid    └─────┘└─┘   └──┘   └┘  └───────────┘                   └──┘  
st   ───────────────────────────┘└─────────────────────────────────────┘└─
420    have ub : ∀ y ∈ S, (y:ℝ) ≤ 1,
id                     
src    └────────┘ └───┘     └┘ └┘
typ    └────────┘ └───┘    └┘ └┘
doc    └────────┘ └───┘     └┘ └┘
txt    └────────┘ └───┘     └┘ └┘
par    └────────┘ └───┘     └┘ └┘
pid    └─────┘└─┘ └───┘     └┘ 
st   ─────────────────────────────┘└─
421    { intros y yS, cases yS with y0 yx,
id                          └┘
src      └─────────┘  └────┘  └─────────┘
typ      └─────────┘  └────┘└┘└─────────┘
doc      └─────────┘  └────┘  └─────────┘
txt      └─────────┘  └────┘  └─────────┘
par      └─────────┘  └────┘  └─────────┘
pid            └───┘         └─────────┘
st   ───┘└─────────┘└───────────────────┘└─
422      refine (mul_self_le_mul_self_iff (le_of_lt y0) zero_le_one).2 _,
id               └──────────────────────┘  └──────┘ └┘  └─────────┘
src      └─────┘ └──────────────────────┘ └──────┘  └┘└─────────┘└───┘
typ      └─────┘ └──────────────────────┘ └──────┘└┘└┘└─────────┘└───┘
doc      └─────┘                                    └┘           └───┘
txt      └─────┘                                    └┘           └───┘
par      └─────┘                                    └┘           └───┘
pid                                                └┘           └───┘
st   ──────────────────────────────────────────────────────────────────┘└─
423      simpa using le_trans yx x1 },
id                   └──────┘ └┘ └┘
src      └──────────┘└──────┘    
typ      └──────────┘└──────┘└┘└┘
doc      └──────────┘            
txt      └──────────┘            
par      └──────────┘            
pid           └────┘            
st   ──────────────────────────────┘└┘
424    have S0 : 0 < Sup S := lt_of_lt_of_le x0 (le_Sup _ ⟨_, ub⟩ lb),
id                   └─┘     └────────────┘ └┘  └────┘       └┘  └┘
src    └──────────┘ └─┘ └──┘└────────────┘   └────┘└─┘ └─┘  └┘  
typ    └──────────┘ └─┘└──┘└────────────┘└┘ └────┘└─┘ └─┘└┘└┘└┘
doc    └──────────┘     └──┘                       └─┘ └─┘  └┘  
txt    └──────────┘     └──┘                       └─┘ └─┘  └┘  
par    └──────────┘     └──┘                       └─┘ └─┘  └┘  
pid    └─────┘└───┘     └──┘                       └─┘ └─┘  └┘  
st   ───────────────────────────────────────────────────────────────┘└─
425    refine ⟨Sup S, S0, le_antisymm (not_lt.1 $ λ h, _) (not_lt.1 $ λ h, _)⟩,
id             └─┘   └┘  └─────────┘                      └────┘
src    └─────┘ └─┘ └┘  └┘└─────────┘       └─┘  └─────┘ └────┘└─┘  └─────┘
typ    └─────┘ └─┘└┘└┘└┘└─────────┘       └─┘  └─────┘ └────┘└─┘  └─────┘
doc    └─────┘     └┘  └┘                  └─┘  └─────┘       └─┘  └─────┘
txt    └─────┘     └┘  └┘                  └─┘  └─────┘       └─┘  └─────┘
par    └─────┘     └┘  └┘                  └─┘  └─────┘       └─┘  └─────┘
pid               └┘  └┘                  └─┘  └─────┘       └─┘  └─────┘
st   ────────────────────────────────────────────────────────────────────────┘└─
426    { rw [← div_lt_iff S0, lt_Sup S ⟨_, lb⟩ ⟨_, ub⟩] at h,
id             └────────┘ └┘  └────┘      └┘      └┘
src      └────┘└────────┘  └┘└────┘  └─┘  └┘ └─┘  └─────┘
typ      └────┘└────────┘└┘└┘└────┘ └─┘└┘└┘ └─┘└┘└─────┘
doc      └────┘            └┘        └─┘  └┘ └─┘  └─────┘
txt      └────┘            └┘        └─┘  └┘ └─┘  └─────┘
par      └────┘            └┘        └─┘  └┘ └─┘  └─────┘
pid        └──┘            └┘        └─┘  └┘ └─┘  └┘└───┘
st   ───┘└─────────────────┘└────────────────────────┘└───┘└─
427      rcases h with ⟨y, ⟨y0, yx⟩, hy⟩,
id              
src      └─────┘ └─────────────────────┘
typ      └─────┘└─────────────────────┘
doc      └─────┘ └─────────────────────┘
txt      └─────┘ └─────────────────────┘
par      └─────┘ └─────────────────────┘
pid             └─────────────────────┘
st   ──────────────────────────────────┘└─
428      rw [div_lt_iff S0, ← div_lt_iff' y0, lt_Sup S ⟨_, lb⟩ ⟨_, ub⟩] at hy,
id           └────────┘ └┘    └─────────┘ └┘  └────┘      └┘      └┘
src      └──┘└────────┘  └──┘└─────────┘  └┘└────┘  └─┘  └┘ └─┘  └──────┘
typ      └──┘└────────┘└┘└──┘└─────────┘└┘└┘└────┘ └─┘└┘└┘ └─┘└┘└──────┘
doc      └──┘            └──┘             └┘        └─┘  └┘ └─┘  └──────┘
txt      └──┘            └──┘             └┘        └─┘  └┘ └─┘  └──────┘
par      └──┘            └──┘             └┘        └─┘  └┘ └─┘  └──────┘
pid        └┘            └──┘             └┘        └─┘  └┘ └─┘  └┘└────┘
st   ────────────────────┘└────────────────┘└────────────────────────┘└────┘└─
429      rcases hy with ⟨z, ⟨z0, zx⟩, hz⟩,
id              └┘
src      └─────┘  └─────────────────────┘
typ      └─────┘└┘└─────────────────────┘
doc      └─────┘  └─────────────────────┘
txt      └─────┘  └─────────────────────┘
par      └─────┘  └─────────────────────┘
pid              └─────────────────────┘
st   ───────────────────────────────────┘└─
430      rw [div_lt_iff y0] at hz,
id           └────────┘ └┘
src      └──┘└────────┘  └─────┘
typ      └──┘└────────┘└┘└─────┘
doc      └──┘            └─────┘
txt      └──┘            └─────┘
par      └──┘            └─────┘
pid        └┘            └────┘
st   ────────────────────┘└────┘└─
431      exact not_lt_of_lt
id             └──────────┘
src      └────┘└──────────┘
typ      └────┘└──────────┘
doc      └────┘            
txt      └────┘            
par      └────┘            
pid                       
st   ───────────────────────
432        ((mul_lt_mul_right y0).1 (lt_of_le_of_lt yx hz))
id           └──────────────┘ └┘                    └┘
src  ─────┘  └──────────────┘  └──┘                   └──
typ  ─────┘  └──────────────┘└┘└──┘               └┘  └──
doc  ─────┘                    └──┘                   └──
txt  ─────┘                    └──┘                   └──
par  ─────┘                    └──┘                   └──
pid  ─────┘                    └──┘                   └──
st   ───────────────────────────────────────────────────────
433        ((mul_lt_mul_left z0).1 (lt_of_le_of_lt zx hz)) },
id           └─────────────┘ └┘     └────────────┘ └┘ └┘
src  ─────┘  └─────────────┘  └──┘ └────────────┘    └─┘
typ  ─────┘  └─────────────┘└┘└──┘ └────────────┘└┘└┘└─┘
doc  ─────┘                   └──┘                   └─┘
txt  ─────┘                   └──┘                   └─┘
par  ─────┘                   └──┘                   └─┘
pid  ─────┘                   └──┘                   └┘
st   ─────────────────────────────────────────────────────┘└┘
434    { let s := Sup S, let y := s + (x - s * s) / 3,
id                └─┘                        
src      └───────┘└─┘   └───────┘      └┘└┘
typ      └───────┘└─┘  └───────┘    └┘└┘
doc      └───────┘      └───────┘        └┘ └┘
txt      └───────┘      └───────┘        └┘ └┘
par      └───────┘      └───────┘        └┘ └┘
pid      └───┘└─┘      └───┘└─┘        └┘ 
st   ─────────────────┘└────────────────────────────┘└─
435      replace h : 0 < x - s * s := sub_pos.2 h,
id                                  └─────┘   
src      └────────────┘      └──┘└─────┘└─┘
typ      └────────────┘    └──┘└─────┘└─┘
doc      └────────────┘      └──┘       └─┘
txt      └────────────┘      └──┘       └─┘
par      └────────────┘      └──┘       └─┘
pid             └┘└───┘      └──┘       └─┘
st   ───────────────────────────────────────────┘└─
436      have _30 := bit1_pos zero_le_one,
id                   └──────┘ └─────────┘
src      └──────────┘└──────┘└─────────┘
typ      └──────────┘└──────┘└─────────┘
doc      └──────────┘        
txt      └──────────┘        
par      └──────────┘        
pid      └──────┘└─┘        
st   ───────────────────────────────────┘└─
437      have : s < y := (lt_add_iff_pos_right _).2 (div_pos h _30),
id                      └──────────────────┘       └─────┘  └─┘
src      └─────┘   └──┘ └──────────────────┘└────┘ └─────┘    
typ      └─────┘ └──┘ └──────────────────┘└────┘ └─────┘└─┘
doc      └─────┘   └──┘                     └────┘            
txt      └─────┘   └──┘                     └────┘            
par      └─────┘   └──┘                     └────┘            
pid      └───┘└┘   └──┘                     └────┘            
st   ─────────────────────────────────────────────────────────────┘└─
438      refine not_le_of_lt this (le_Sup S ⟨_, ub⟩ ⟨lt_trans S0 this, _⟩),
id              └──────────┘       └────┘      └┘   └──────┘ └┘ └──┘
src      └─────┘└──────────┘     └────┘  └─┘  └┘ └──────┘      └───┘
typ      └─────┘└──────────┘     └────┘ └─┘└┘└┘ └──────┘└┘└──┘└───┘
doc      └─────┘                         └─┘  └┘               └───┘
txt      └─────┘                         └─┘  └┘               └───┘
par      └─────┘                         └─┘  └┘               └───┘
pid                                     └─┘  └┘               └───┘
st   ────────────────────────────────────────────────────────────────────┘└─
439      rw [add_mul_self_eq, add_assoc, ← le_sub_iff_add_le', ← add_mul,
id           └─────────────┘  └───────┘    └────────────────┘    └─────┘
src      └──┘└─────────────┘└┘└───────┘└──┘└────────────────┘└──┘└─────┘└─
typ      └──┘└─────────────┘└┘└───────┘└──┘└────────────────┘└──┘└─────┘└─
doc      └──┘               └┘         └──┘                  └──┘       └─
txt      └──┘               └┘         └──┘                  └──┘       └─
par      └──┘               └┘         └──┘                  └──┘       └─
pid        └┘               └┘         └──┘                  └──┘       └─
st   ──────────────────────┘└─────────┘└────────────────────┘└─────────┘└─
440        ← le_div_iff (div_pos h _30), div_div_cancel (ne_of_gt h)],
id           └────────┘  └─────┘  └─┘   └────────────┘  └──────┘ 
src  ───────┘└────────┘ └─────┘    └─┘└────────────┘ └──────┘ └┘
typ  ───────┘└────────┘ └─────┘└─┘└─┘└────────────┘ └──────┘└┘
doc  ───────┘                      └─┘                        └┘
txt  ───────┘                      └─┘                        └┘
par  ───────┘                      └─┘                        └┘
pid  ───────┘                      └─┘                        └┘
st   ─────────────────────────────────┘└───────────────────────────┘└──
441      apply add_le_add,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
442      { simpa using (mul_le_mul_left (@two_pos ℝ _)).2 (Sup_le_ub _ ⟨_, lb⟩ ub) },
id                      └─────────────┘   └─────┘          └───────┘       └┘  └┘
src        └──────────┘ └─────────────┘  └─────┘ └─────┘ └───────┘└─┘ └─┘  └┘  └┘
typ        └──────────┘ └─────────────┘  └─────┘ └─────┘ └───────┘└─┘ └─┘└┘└┘└┘└┘
doc        └──────────┘                          └─────┘          └─┘ └─┘  └┘  └┘
txt        └──────────┘                          └─────┘          └─┘ └─┘  └┘  └┘
par        └──────────┘                          └─────┘          └─┘ └─┘  └┘  └┘
pid             └────┘                          └─────┘          └─┘ └─┘  └┘  
st   ─────┘└──────────────────────────────────────────────────────────────────────┘└┘
443      { rw [div_le_one_iff_le _30],
id             └───────────────┘ └─┘
src        └──┘└───────────────┘   
typ        └──┘└───────────────┘└─┘
doc        └──┘                    
txt        └──┘                    
par        └──┘                    
pid          └┘                    
st   ──────────────────────────────┘└──
444        refine le_trans (sub_le_self _ (mul_self_nonneg _)) (le_trans x1 _),
id                          └─────────┘    └─────────────┘      └──────┘ └┘
src        └─────┘         └─────────┘└─┘ └─────────────┘└───┘ └──────┘  └─┘
typ        └─────┘         └─────────┘└─┘ └─────────────┘└───┘ └──────┘└┘└─┘
doc        └─────┘                    └─┘                └───┘           └─┘
txt        └─────┘                    └─┘                └───┘           └─┘
par        └─────┘                    └─┘                └───┘           └─┘
pid                                  └─┘                └───┘           └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
445        exact (le_add_iff_nonneg_left _).2 (le_of_lt two_pos) } }
id                └────────────────────┘       └──────┘ └─────┘
src        └────┘ └────────────────────┘└────┘ └──────┘└─────┘└┘
typ        └────┘ └────────────────────┘└────┘ └──────┘└─────┘└┘
doc        └────┘                       └────┘                └┘
txt        └────┘                       └────┘                └┘
par        └────┘                       └────┘                └┘
pid                                    └────┘                
st   ───────────────────────────────────────────────────────────┘└───
446  end
st   ──┘
447  
448  def sqrt_aux (f : cau_seq ℚ abs) : ℕ → ℚ
id                     └─────┘  └─┘      
src                    └─────┘  └─┘       
typ                    └─────┘  └─┘      
doc                                        
449  | 0       := rat.mk_nat (f 0).num.to_nat.sqrt (f 0).denom.sqrt
id                └────────┘     └─┘ └────┘ └──┘      └───┘ └──┘
src               └────────┘      └─┘ └────┘ └──┘       └───┘ └──┘
typ               └────────┘     └─┘ └────┘ └──┘      └───┘ └──┘
doc               └────────┘                 └──┘             └──┘
450  | (n + 1) := let s := sqrt_aux n in max 0 $ (s + f (n+1) / s) / 2
id                      └──────┘      └─┘                 
src                                     └─┘                    
typ                     └──────┘      └─┘                 
451  
452  theorem sqrt_aux_nonneg (f : cau_seq ℚ abs) : ∀ i : ℕ, 0 ≤ sqrt_aux f i
id                                └─────┘  └─┘              └──────┘  
src                               └─────┘  └─┘               └──────┘
typ                               └─────┘  └─┘              └──────┘  
doc                                       
453  | 0       := by rw [sqrt_aux, mk_nat_eq, mk_eq_div];
id                       └──────┘  └───────┘  └───────┘
src                  └──┘└──────┘└┘└───────┘└┘└───────┘
typ                  └──┘└──────┘└┘└───────┘└┘└───────┘
doc                  └──┘        └┘         └┘         
txt                  └──┘        └┘         └┘         
par                  └──┘        └┘         └┘         
pid                    └┘        └┘         └┘         
st                  └───────────┘└─────────┘└─────────┘└─
454    apply div_nonneg'; exact int.cast_nonneg.2 (int.of_nat_nonneg _)
id           └─────────┘        └─────────────┘    └───────────────┘
src    └────┘└─────────┘  └────┘└─────────────┘└─┘ └───────────────┘└──┘
typ    └────┘└─────────┘  └────┘└─────────────┘└─┘ └───────────────┘└──┘
doc    └────┘             └────┘               └─┘                  └──┘
txt    └────┘             └────┘               └─┘                  └──┘
par    └────┘             └────┘               └─┘                  └──┘
pid                                          └─┘                  └─┘
st   ──────────────────────────────────────────────────────────────────┘
455  | (n + 1) := le_max_left _ _
id               └─────────┘
src              └─────────┘
typ              └─────────┘
456  
457  /- TODO(Mario): finish the proof
458  theorem sqrt_aux_converges (f : cau_seq ℚ abs) : ∃ h x, 0 ≤ x ∧ x * x = max 0 (mk f) ∧
459    mk ⟨sqrt_aux f, h⟩ = x :=
460  begin
461    rcases sqrt_exists (le_max_left 0 (mk f)) with ⟨x, x0, hx⟩,
462    suffices : ∃ h, mk ⟨sqrt_aux f, h⟩ = x,
463    { exact this.imp (λ h e, ⟨x, x0, hx, e⟩) },
464    apply of_near,
465  
466    suffices : ∃ δ > 0, ∀ i, abs (↑(sqrt_aux f i) - x) < δ / 2 ^ i,
467    { rcases this with ⟨δ, δ0, hδ⟩,
468      intros,
469       }
470  end -/
471  
472  noncomputable def sqrt (x : ℝ) : ℝ :=
id                                   
src                                  
typ                                  
473  classical.some (sqrt_exists (le_max_left 0 x))
id   └────────────┘  └─────────┘  └─────────┘   
src  └────────────┘  └─────────┘  └─────────┘
typ  └────────────┘  └─────────┘  └─────────┘   
474  /-quotient.lift_on x
475    (λ f, mk ⟨sqrt_aux f, (sqrt_aux_converges f).fst⟩)
476    (λ f g e, begin
477      rcases sqrt_aux_converges f with ⟨hf, x, x0, xf, xs⟩,
478      rcases sqrt_aux_converges g with ⟨hg, y, y0, yg, ys⟩,
479      refine xs.trans (eq.trans _ ys.symm),
480      rw [← @mul_self_inj_of_nonneg ℝ _ x y x0 y0, xf, yg],
481      congr' 1, exact quotient.sound e
482    end)-/
483  
484  theorem sqrt_prop (x : ℝ) : 0 ≤ sqrt x ∧ sqrt x * sqrt x = max 0 x :=
id                                 └──┘   └──┘   └──┘   └─┘   
src                                └──┘    └──┘    └──┘    └─┘
typ                                └──┘   └──┘   └──┘   └─┘   
485  classical.some_spec (sqrt_exists (le_max_left 0 x))
id   └─────────────────┘  └─────────┘  └─────────┘   
src  └─────────────────┘  └─────────┘  └─────────┘
typ  └─────────────────┘  └─────────┘  └─────────┘   
486  /-quotient.induction_on x $ λ f,
487  by rcases sqrt_aux_converges f with ⟨hf, _, x0, xf, rfl⟩; exact ⟨x0, xf⟩-/
488  
489  theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0 :=
id                                              └──┘  
src                                              └──┘   
typ                                             └──┘  
490  eq_zero_of_mul_self_eq_zero $ (sqrt_prop x).2.trans $ max_eq_left h
id   └─────────────────────────┘    └───────┘   └───┘    └─────────┘ 
src  └─────────────────────────┘    └───────┘    └───┘    └─────────┘
typ  └─────────────────────────┘    └───────┘   └───┘    └─────────┘ 
491  
492  theorem sqrt_nonneg (x : ℝ) : 0 ≤ sqrt x := (sqrt_prop x).1
id                                   └──┘      └───────┘  
src                                  └──┘       └───────┘   
typ                                  └──┘      └───────┘  
493  
494  @[simp] theorem mul_self_sqrt (h : 0 ≤ x) : sqrt x * sqrt x = x :=
id                                             └──┘   └──┘   
src                                             └──┘    └──┘   
typ                                            └──┘   └──┘   
doc    └──┘
495  (sqrt_prop x).2.trans (max_eq_right h)
id    └───────┘   └───┘   └──────────┘ 
src   └───────┘    └───┘   └──────────┘
typ   └───────┘   └───┘   └──────────┘ 
496  
497  @[simp] theorem sqrt_mul_self (h : 0 ≤ x) : sqrt (x * x) = x :=
id                                             └──┘       
src                                             └──┘        
typ                                            └──┘       
doc    └──┘
498  (mul_self_inj_of_nonneg (sqrt_nonneg _) h).1 (mul_self_sqrt (mul_self_nonneg _))
id    └────────────────────┘  └─────────┘        └───────────┘  └─────────────┘
src   └────────────────────┘  └─────────┘         └───────────┘  └─────────────┘
typ   └────────────────────┘  └─────────┘        └───────────┘  └─────────────┘
499  
500  theorem sqrt_eq_iff_mul_self_eq (hx : 0 ≤ x) (hy : 0 ≤ y) :
id                                                       
src                                                      
typ                                                      
501    sqrt x = y ↔ y * y = x :=
id     └──┘         
src    └──┘            
typ    └──┘         
502  ⟨λ h, by rw [← h, mul_self_sqrt hx],
id                   └───────────┘ └┘
src           └────┘ └┘└───────────┘  
typ          └────┘└┘└───────────┘└┘
doc           └────┘ └┘               
txt           └────┘ └┘               
par           └────┘ └┘               
pid             └──┘ └┘               
st           └──────┘└────────────────┘
503   λ h, by rw [← h, sqrt_mul_self hy]⟩
id                   └───────────┘ └┘
src           └────┘ └┘└───────────┘  
typ          └────┘└┘└───────────┘└┘
doc           └────┘ └┘               
txt           └────┘ └┘               
par           └────┘ └┘               
pid             └──┘ └┘               
st           └──────┘└────────────────┘
504  
505  @[simp] theorem sqr_sqrt (h : 0 ≤ x) : sqrt x ^ 2 = x :=
id                                        └──┘      
src                                        └──┘      
typ                                       └──┘      
doc    └──┘
506  by rw [pow_two, mul_self_sqrt h]
id          └─────┘  └───────────┘ 
src     └──┘└─────┘└┘└───────────┘ └─
typ     └──┘└─────┘└┘└───────────┘└─
doc     └──┘       └┘              └─
txt     └──┘       └┘              └─
par     └──┘       └┘              └─
pid       └┘       └┘              
st     └──────────┘└───────────────┘
507  
src  
typ  
doc  
txt  
par  
pid  
st   
508  @[simp] theorem sqrt_sqr (h : 0 ≤ x) : sqrt (x ^ 2) = x :=
id                                        └──┘        
src                                        └──┘        
typ                                       └──┘        
doc    └──┘
509  by rw [pow_two, sqrt_mul_self h]
id          └─────┘  └───────────┘ 
src     └──┘└─────┘└┘└───────────┘ └─
typ     └──┘└─────┘└┘└───────────┘└─
doc     └──┘       └┘              └─
txt     └──┘       └┘              └─
par     └──┘       └┘              └─
pid       └┘       └┘              
st     └──────────┘└───────────────┘
510  
src  
typ  
doc  
txt  
par  
pid  
st   
511  theorem sqrt_eq_iff_sqr_eq (hx : 0 ≤ x) (hy : 0 ≤ y) :
id                                                  
src                                                 
typ                                                 
512    sqrt x = y ↔ y ^ 2 = x :=
id     └──┘          
src    └──┘            
typ    └──┘          
513  by rw [pow_two, sqrt_eq_iff_mul_self_eq hx hy]
id          └─────┘  └─────────────────────┘ └┘ └┘
src     └──┘└─────┘└┘└─────────────────────┘    └─
typ     └──┘└─────┘└┘└─────────────────────┘└┘└┘└─
doc     └──┘       └┘                           └─
txt     └──┘       └┘                           └─
par     └──┘       └┘                           └─
pid       └┘       └┘                           
st     └──────────┘└─────────────────────────────┘
514  
src  
typ  
doc  
txt  
par  
pid  
st   
515  theorem sqrt_mul_self_eq_abs (x : ℝ) : sqrt (x * x) = abs x :=
id                                         └──┘       └─┘ 
src                                        └──┘         └─┘
typ                                        └──┘       └─┘ 
516  (le_total 0 x).elim
id    └──────┘    └──┘
src   └──────┘     └──┘
typ   └──────┘    └──┘
517    (λ h, (sqrt_mul_self h).trans (abs_of_nonneg h).symm)
id           └───────────┘  └───┘   └───────────┘  └──┘
src           └───────────┘   └───┘   └───────────┘   └──┘
typ          └───────────┘  └───┘   └───────────┘  └──┘
518    (λ h, by rw [← neg_mul_neg,
id                   └─────────┘
src             └────┘└─────────┘└─
typ            └────┘└─────────┘└─
doc             └────┘           └─
txt             └────┘           └─
par             └────┘           └─
pid               └──┘           └─
st             └────────────────┘└─
519      sqrt_mul_self (neg_nonneg.2 h), abs_of_nonpos h])
id       └───────────┘  └────────┘      └───────────┘ 
src  ───┘└───────────┘ └────────┘└─┘ └─┘└───────────┘ 
typ  ───┘└───────────┘ └────────┘└─┘└─┘└───────────┘
doc  ───┘                        └─┘ └─┘              
txt  ───┘                        └─┘ └─┘              
par  ───┘                        └─┘ └─┘              
pid  ───┘                        └─┘ └─┘              
st   ─────────────────────────────────┘└───────────────┘
520  
521  theorem sqrt_sqr_eq_abs (x : ℝ) : sqrt (x ^ 2) = abs x :=
id                                    └──┘        └─┘ 
src                                   └──┘         └─┘
typ                                   └──┘        └─┘ 
522  by rw [pow_two, sqrt_mul_self_eq_abs]
id          └─────┘  └──────────────────┘
src     └──┘└─────┘└┘└──────────────────┘└─
typ     └──┘└─────┘└┘└──────────────────┘└─
doc     └──┘       └┘                    └─
txt     └──┘       └┘                    └─
par     └──┘       └┘                    └─
pid       └┘       └┘                    
st     └──────────┘└────────────────────┘
523  
src  
typ  
doc  
txt  
par  
pid  
st   
524  @[simp] theorem sqrt_zero : sqrt 0 = 0 :=
id                               └──┘   
src                              └──┘   
typ                              └──┘   
doc    └──┘
525  by simpa using sqrt_mul_self (le_refl _)
id                  └───────────┘  └─────┘
src     └──────────┘└───────────┘ └─────┘└───
typ     └──────────┘└───────────┘ └─────┘└───
doc     └──────────┘                     └───
txt     └──────────┘                     └───
par     └──────────┘                     └───
pid          └────┘                     └─┘
st     └──────────────────────────────────────
526  
src  
typ  
doc  
txt  
par  
pid  
st   
527  @[simp] theorem sqrt_one : sqrt 1 = 1 :=
id                              └──┘   
src                             └──┘   
typ                             └──┘   
doc    └──┘
528  by simpa using sqrt_mul_self zero_le_one
id                  └───────────┘ └─────────┘
src     └──────────┘└───────────┘└─────────┘
typ     └──────────┘└───────────┘└─────────┘
doc     └──────────┘                        
txt     └──────────┘                        
par     └──────────┘                        
pid          └────┘                        
st     └──────────────────────────────────────
529  
src  
typ  
doc  
txt  
par  
pid  
st   
530  @[simp] theorem sqrt_le (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x ≤ sqrt y ↔ x ≤ y :=
id                                                   └──┘   └──┘     
src                                                    └──┘    └──┘      
typ                                                  └──┘   └──┘     
doc    └──┘
531  by rw [mul_self_le_mul_self_iff (sqrt_nonneg _) (sqrt_nonneg _),
id          └──────────────────────┘                  └─────────┘
src     └──┘└──────────────────────┘            └──┘ └─────────┘└────
typ     └──┘└──────────────────────┘            └──┘ └─────────┘└────
doc     └──┘                                    └──┘            └────
txt     └──┘                                    └──┘            └────
par     └──┘                                    └──┘            └────
pid       └┘                                    └──┘            └────
st     └───────────────────────────────────────────────────────────┘└─
532         mul_self_sqrt hx, mul_self_sqrt hy]
id          └───────────┘ └┘  └───────────┘ └┘
src  ──────┘└───────────┘  └┘└───────────┘  └─
typ  ──────┘└───────────┘└┘└┘└───────────┘└┘└─
doc  ──────┘               └┘               └─
txt  ──────┘               └┘               └─
par  ──────┘               └┘               └─
pid  ──────┘               └┘               
st   ──────────────────────┘└────────────────┘
533  
src  
typ  
doc  
txt  
par  
pid  
st   
534  @[simp] theorem sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x < sqrt y ↔ x < y :=
id                                                   └──┘   └──┘     
src                                                    └──┘    └──┘      
typ                                                  └──┘   └──┘     
doc    └──┘
535  lt_iff_lt_of_le_iff_le (sqrt_le hy hx)
id   └────────────────────┘  └─────┘ └┘ └┘
src  └────────────────────┘  └─────┘
typ  └────────────────────┘  └─────┘ └┘ └┘
536  
537  lemma sqrt_le_sqrt (h : x ≤ y) : sqrt x ≤ sqrt y :=
id                                 └──┘   └──┘ 
src                                  └──┘    └──┘
typ                                └──┘   └──┘ 
538  begin
st   └─────
539    rw [mul_self_le_mul_self_iff (sqrt_nonneg _) (sqrt_nonneg _), (sqrt_prop _).2, (sqrt_prop _).2],
id         └──────────────────────┘                  └─────────┘      └───────┘        └───────┘
src    └──┘└──────────────────────┘            └──┘ └─────────┘└───┘ └───────┘└─────┘ └───────┘└────┘
typ    └──┘└──────────────────────┘            └──┘ └─────────┘└───┘ └───────┘└─────┘ └───────┘└────┘
doc    └──┘                                    └──┘            └───┘          └─────┘          └────┘
txt    └──┘                                    └──┘            └───┘          └─────┘          └────┘
par    └──┘                                    └──┘            └───┘          └─────┘          └────┘
pid      └┘                                    └──┘            └───┘          └─────┘          └────┘
st   ─────────────────────────────────────────────────────────────┘└─────────────┘└───────────────┘└────
540    exact max_le_max (le_refl _) h
id           └────────┘  └─────┘    
src    └────┘└────────┘ └─────┘└──┘ 
typ    └────┘└────────┘ └─────┘└──┘
doc    └────┘                  └──┘ 
txt    └────┘                  └──┘ 
par    └────┘                  └──┘ 
pid                           └──┘ 
st   ────────────────────────────────┘
541  end
st   └─┘
542  
543  lemma sqrt_le_left (hy : 0 ≤ y) : sqrt x ≤ y ↔ x ≤ y ^ 2 :=
id                                   └──┘        
src                                   └──┘            
typ                                  └──┘        
544  begin
st   └─────
545    rw [mul_self_le_mul_self_iff (sqrt_nonneg _) hy, pow_two],
id         └──────────────────────┘  └─────────┘    └┘  └─────┘
src    └──┘└──────────────────────┘ └─────────┘└──┘  └┘└─────┘
typ    └──┘└──────────────────────┘ └─────────┘└──┘└┘└┘└─────┘
doc    └──┘                                    └──┘  └┘       
txt    └──┘                                    └──┘  └┘       
par    └──┘                                    └──┘  └┘       
pid      └┘                                    └──┘  └┘       
st   ────────────────────────────────────────────────┘└───────┘└──
546    cases le_total 0 x with hx hx,
id           └──────┘   
src    └────┘└──────┘└─┘ └─────────┘
typ    └────┘└──────┘└─┘└─────────┘
doc    └────┘        └─┘ └─────────┘
txt    └────┘        └─┘ └─────────┘
par    └────┘        └─┘ └─────────┘
pid                 └─┘ └─────────┘
st   ──────────────────────────────┘└─
547    { rw [mul_self_sqrt hx] },
id           └───────────┘ └┘
src      └──┘└───────────┘  └┘
typ      └──┘└───────────┘└┘└┘
doc      └──┘               └┘
txt      └──┘               └┘
par      └──┘               └┘
pid        └┘               
st   ───┘└──────────────────┘└┘
548    { have h1 : 0 ≤ y * y := mul_nonneg hy hy,
id                           └────────┘    └┘
src      └──────────┘  └──┘└────────┘  
typ      └──────────┘ └──┘└────────┘  └┘
doc      └──────────┘    └──┘            
txt      └──────────┘    └──┘            
par      └──────────┘    └──┘            
pid      └─────┘└───┘    └──┘            
st   ──────────────────────────────────────────┘└─
549      have h2 : x ≤ y * y := le_trans hx h1,
id                            └──────┘ └┘ └┘
src      └────────┘     └──┘└──────┘  
typ      └────────┘   └──┘└──────┘└┘└┘
doc      └────────┘     └──┘          
txt      └────────┘     └──┘          
par      └────────┘     └──┘          
pid      └─────┘└─┘     └──┘          
st   ────────────────────────────────────────┘└─
550      simp [sqrt_eq_zero_of_nonpos, hx, h1, h2] }
id             └────────────────────┘  └┘  └┘  └┘
src      └────┘└────────────────────┘└┘  └┘  └┘  └┘
typ      └────┘└────────────────────┘└┘└┘└┘└┘└┘└┘└┘
doc      └────┘                      └┘  └┘  └┘  └┘
txt      └────┘                      └┘  └┘  └┘  └┘
par      └────┘                      └┘  └┘  └┘  └┘
pid                                └┘  └┘  └┘  
st   ─────────────────────────────────────────────┘└─
551  end
st   ──┘
552  
553  /- note: if you want to conclude `x ≤ sqrt y`, then use `le_sqrt_of_sqr_le`.
554     if you have `x > 0`, consider using `le_sqrt'` -/
555  lemma le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
id                                           └──┘        
src                                             └──┘         
typ                                          └──┘        
556  by rw [mul_self_le_mul_self_iff hx (sqrt_nonneg _), pow_two, mul_self_sqrt hy]
id          └──────────────────────┘ └┘  └─────────┘     └─────┘  └───────────┘ └┘
src     └──┘└──────────────────────┘   └─────────┘└───┘└─────┘└┘└───────────┘  └─
typ     └──┘└──────────────────────┘└┘ └─────────┘└───┘└─────┘└┘└───────────┘└┘└─
doc     └──┘                                      └───┘       └┘               └─
txt     └──┘                                      └───┘       └┘               └─
par     └──┘                                      └───┘       └┘               └─
pid       └┘                                      └───┘       └┘               
st     └──────────────────────────────────────────────┘└───────┘└────────────────┘
557  
src  
typ  
doc  
txt  
par  
pid  
st   
558  lemma le_sqrt' (hx : 0 < x) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
id                                 └──┘        
src                                  └──┘         
typ                                └──┘        
559  begin
st   └─────
560    rw [mul_self_le_mul_self_iff (le_of_lt hx) (sqrt_nonneg _), pow_two],
id         └──────────────────────┘  └──────┘ └┘   └─────────┘     └─────┘
src    └──┘└──────────────────────┘ └──────┘  └┘ └─────────┘└───┘└─────┘
typ    └──┘└──────────────────────┘ └──────┘└┘└┘ └─────────┘└───┘└─────┘
doc    └──┘                                   └┘            └───┘       
txt    └──┘                                   └┘            └───┘       
par    └──┘                                   └┘            └───┘       
pid      └┘                                   └┘            └───┘       
st   ───────────────────────────────────────────────────────────┘└───────┘└──
561    cases le_total 0 y with hy hy,
id           └──────┘   
src    └────┘└──────┘└─┘ └─────────┘
typ    └────┘└──────┘└─┘└─────────┘
doc    └────┘        └─┘ └─────────┘
txt    └────┘        └─┘ └─────────┘
par    └────┘        └─┘ └─────────┘
pid                 └─┘ └─────────┘
st   ──────────────────────────────┘└─
562    { rw [mul_self_sqrt hy] },
id           └───────────┘ └┘
src      └──┘└───────────┘  └┘
typ      └──┘└───────────┘└┘└┘
doc      └──┘               └┘
txt      └──┘               └┘
par      └──┘               └┘
pid        └┘               
st   ───┘└──────────────────┘└┘
563    { have h1 : 0 < x * x := mul_pos hx hx,
id                           └─────┘    └┘
src      └──────────┘  └──┘└─────┘  
typ      └──────────┘ └──┘└─────┘  └┘
doc      └──────────┘    └──┘         
txt      └──────────┘    └──┘         
par      └──────────┘    └──┘         
pid      └─────┘└───┘    └──┘         
st   ───────────────────────────────────────┘└─
564      have h2 : ¬x * x ≤ y := not_le_of_lt (lt_of_le_of_lt hy h1),
id                           └──────────┘  └────────────┘ └┘ └┘
src      └────────┘    └──┘└──────────┘ └────────────┘    
typ      └────────┘  └──┘└──────────┘ └────────────┘└┘└┘
doc      └────────┘      └──┘                               
txt      └────────┘      └──┘                               
par      └────────┘      └──┘                               
pid      └─────┘└─┘      └──┘                               
st   ──────────────────────────────────────────────────────────────┘└─
565      simp [sqrt_eq_zero_of_nonpos, hy, h1, h2] }
id             └────────────────────┘  └┘  └┘  └┘
src      └────┘└────────────────────┘└┘  └┘  └┘  └┘
typ      └────┘└────────────────────┘└┘└┘└┘└┘└┘└┘└┘
doc      └────┘                      └┘  └┘  └┘  └┘
txt      └────┘                      └┘  └┘  └┘  └┘
par      └────┘                      └┘  └┘  └┘  └┘
pid                                └┘  └┘  └┘  
st   ─────────────────────────────────────────────┘└─
566  end
st   ──┘
567  
568  lemma le_sqrt_of_sqr_le (h : x ^ 2 ≤ y) : x ≤ sqrt y :=
id                                           └──┘ 
src                                             └──┘
typ                                          └──┘ 
569  begin
st   └─────
570    cases lt_or_ge 0 x with hx hx,
id           └──────┘   
src    └────┘└──────┘└─┘ └─────────┘
typ    └────┘└──────┘└─┘└─────────┘
doc    └────┘        └─┘ └─────────┘
txt    └────┘        └─┘ └─────────┘
par    └────┘        └─┘ └─────────┘
pid                 └─┘ └─────────┘
st   ──────────────────────────────┘└─
571    { rwa [le_sqrt' hx] },
id            └──────┘ └┘
src      └───┘└──────┘  └┘
typ      └───┘└──────┘└┘└┘
doc      └───┘          └┘
txt      └───┘          └┘
par      └───┘          └┘
pid         └┘          
st   ───┘└──────────────┘└┘
572    { exact le_trans hx (sqrt_nonneg y) }
id             └──────┘ └┘  └─────────┘ 
src      └────┘└──────┘   └─────────┘ └┘
typ      └────┘└──────┘└┘ └─────────┘└┘
doc      └────┘                       └┘
txt      └────┘                       └┘
par      └────┘                       └┘
pid                                  
st   ─────────────────────────────────────┘└─
573  end
st   ──┘
574  
575  @[simp] theorem sqrt_inj (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x = sqrt y ↔ x = y :=
id                                                    └──┘   └──┘     
src                                                     └──┘    └──┘      
typ                                                   └──┘   └──┘     
doc    └──┘
576  by simp [le_antisymm_iff, hx, hy]
id            └─────────────┘  └┘  └┘
src     └────┘└─────────────┘└┘  └┘  └─
typ     └────┘└─────────────┘└┘└┘└┘└┘└─
doc     └────┘               └┘  └┘  └─
txt     └────┘               └┘  └┘  └─
par     └────┘               └┘  └┘  └─
pid                        └┘  └┘  
st     └───────────────────────────────
577  
src  
typ  
doc  
txt  
par  
pid  
st   
578  @[simp] theorem sqrt_eq_zero (h : 0 ≤ x) : sqrt x = 0 ↔ x = 0 :=
id                                            └──┘       
src                                            └──┘         
typ                                           └──┘       
doc    └──┘
579  by simpa using sqrt_inj h (le_refl _)
id                  └──────┘   └─────┘
src     └──────────┘└──────┘  └─────┘└───
typ     └──────────┘└──────┘ └─────┘└───
doc     └──────────┘                 └───
txt     └──────────┘                 └───
par     └──────────┘                 └───
pid          └────┘                 └─┘
st     └───────────────────────────────────
580  
src  
typ  
doc  
txt  
par  
pid  
st   
581  theorem sqrt_eq_zero' : sqrt x = 0 ↔ x ≤ 0 :=
id                           └──┘       
src                          └──┘         
typ                          └──┘       
582  (le_total x 0).elim
id    └──────┘    └──┘
src   └──────┘     └──┘
typ   └──────┘    └──┘
583    (λ h, by simp [h, sqrt_eq_zero_of_nonpos])
id                     └────────────────────┘
src             └────┘ └┘└────────────────────┘
typ            └────┘└┘└────────────────────┘
doc             └────┘ └┘                      
txt             └────┘ └┘                      
par             └────┘ └┘                      
pid                  └┘                      
st             └───────────────────────────────┘
584    (λ h, by simp [h]; simp [le_antisymm_iff, h])
id                            └─────────────┘  
src             └────┘   └────┘└─────────────┘└┘ 
typ            └────┘  └────┘└─────────────┘└┘
doc             └────┘   └────┘               └┘ 
txt             └────┘   └────┘               └┘ 
par             └────┘   └────┘               └┘ 
pid                                       └┘ 
st             └──────────────────────────────────┘
585  
586  @[simp] theorem sqrt_pos : 0 < sqrt x ↔ 0 < x :=
id                                 └──┘      
src                                └──┘      
typ                                └──┘      
doc    └──┘
587  lt_iff_lt_of_le_iff_le (iff.trans
id   └────────────────────┘  └───────┘
src  └────────────────────┘  └───────┘
typ  └────────────────────┘  └───────┘
588    (by simp [le_antisymm_iff, sqrt_nonneg]) sqrt_eq_zero')
id               └─────────────┘  └─────────┘   └───────────┘
src        └────┘└─────────────┘└┘└─────────┘  └───────────┘
typ        └────┘└─────────────┘└┘└─────────┘  └───────────┘
doc        └────┘               └┘           
txt        └────┘               └┘           
par        └────┘               └┘           
pid                           └┘           
st        └──────────────────────────────────┘
589  
590  @[simp] theorem sqrt_mul' (x) {y : ℝ} (hy : 0 ≤ y) : sqrt (x * y) = sqrt x * sqrt y :=
id                                                     └──┘       └──┘   └──┘ 
src                                                     └──┘         └──┘    └──┘
typ                                                    └──┘       └──┘   └──┘ 
doc    └──┘
591  begin
st   └─────
592    cases le_total 0 x with hx hx,
id           └──────┘   
src    └────┘└──────┘└─┘ └─────────┘
typ    └────┘└──────┘└─┘└─────────┘
doc    └────┘        └─┘ └─────────┘
txt    └────┘        └─┘ └─────────┘
par    └────┘        └─┘ └─────────┘
pid                 └─┘ └─────────┘
st   ──────────────────────────────┘└─
593    { refine (mul_self_inj_of_nonneg _ (mul_nonneg _ _)).1 _; try {apply sqrt_nonneg},
id               └────────────────────┘    └────────┘                       └─────────┘
src      └─────┘ └────────────────────┘└─┘ └────────┘└────────┘  └───┘└────┘└─────────┘
typ      └─────┘ └────────────────────┘└─┘ └────────┘└────────┘  └───┘└────┘└─────────┘
doc      └─────┘                       └─┘           └────────┘  └───┘└────┘           
txt      └─────┘                       └─┘           └────────┘  └───┘└────┘           
par      └─────┘                       └─┘           └────────┘  └───┘└────┘           
pid                                   └─┘           └────────┘     └──────┘           
st   ───┘└───────────────────────────────────────────────────────────┘└───────────────┘└┘
594      rw [mul_self_sqrt (mul_nonneg hx hy), mul_assoc,
id           └───────────┘  └────────┘ └┘ └┘   └───────┘
src      └──┘└───────────┘ └────────┘    └─┘└───────┘└─
typ      └──┘└───────────┘ └────────┘└┘└┘└─┘└───────┘└─
doc      └──┘                            └─┘         └─
txt      └──┘                            └─┘         └─
par      └──┘                            └─┘         └─
pid        └┘                            └─┘         └─
st   ───────────────────────────────────────┘└─────────┘└─
595          mul_left_comm (sqrt y), mul_self_sqrt hy, ← mul_assoc, mul_self_sqrt hx] },
id           └───────────┘  └──┘    └───────────┘ └┘    └───────┘  └───────────┘ └┘
src  ───────┘└───────────┘ └──┘ └─┘└───────────┘  └──┘└───────┘└┘└───────────┘  └┘
typ  ───────┘└───────────┘ └──┘└─┘└───────────┘└┘└──┘└───────┘└┘└───────────┘└┘└┘
doc  ───────┘                   └─┘               └──┘         └┘               └┘
txt  ───────┘                   └─┘               └──┘         └┘               └┘
par  ───────┘                   └─┘               └──┘         └┘               └┘
pid  ───────┘                   └─┘               └──┘         └┘               
st   ─────────────────────────────┘└────────────────┘└───────────┘└────────────────┘└┘
596    { rw [sqrt_eq_zero'.2 (mul_nonpos_of_nonpos_of_nonneg hx hy),
id           └───────────┘    └────────────────────────────┘ └┘ └┘
src      └──┘└───────────┘└─┘ └────────────────────────────┘    └──
typ      └──┘└───────────┘└─┘ └────────────────────────────┘└┘└┘└──
doc      └──┘             └─┘                                   └──
txt      └──┘             └─┘                                   └──
par      └──┘             └─┘                                   └──
pid        └┘             └─┘                                   └──
st   ─────────────────────────────────────────────────────────────┘└─
597          sqrt_eq_zero'.2 hx, zero_mul] }
id           └───────────┘   └┘  └──────┘
src  ───────┘└───────────┘└─┘  └┘└──────┘└┘
typ  ───────┘└───────────┘└─┘└┘└┘└──────┘└┘
doc  ───────┘             └─┘  └┘        └┘
txt  ───────┘             └─┘  └┘        └┘
par  ───────┘             └─┘  └┘        └┘
pid  ───────┘             └─┘  └┘        
st   ─────────────────────────┘└────────┘└─
598  end
st   ──┘
599  
600  @[simp] theorem sqrt_mul (hx : 0 ≤ x) (y : ℝ) : sqrt (x * y) = sqrt x * sqrt y :=
id                                                └──┘       └──┘   └──┘ 
src                                                └──┘         └──┘    └──┘
typ                                               └──┘       └──┘   └──┘ 
doc    └──┘
601  by rw [mul_comm, sqrt_mul' _ hx, mul_comm]
id          └──────┘  └───────┘   └┘  └──────┘
src     └──┘└──────┘└┘└───────┘└─┘  └┘└──────┘└─
typ     └──┘└──────┘└┘└───────┘└─┘└┘└┘└──────┘└─
doc     └──┘        └┘         └─┘  └┘        └─
txt     └──┘        └┘         └─┘  └┘        └─
par     └──┘        └┘         └─┘  └┘        └─
pid       └┘        └┘         └─┘  └┘        
st     └───────────┘└──────────────┘└────────┘
602  
src  
typ  
doc  
txt  
par  
pid  
st   
603  @[simp] theorem sqrt_inv (x : ℝ) : sqrt x⁻¹ = (sqrt x)⁻¹ :=
id                                     └──┘ └┘   └──┘  └┘
src                                    └──┘  └┘   └──┘   └┘
typ                                    └──┘ └┘   └──┘  └┘
doc    └──┘
604  (le_or_lt x 0).elim
id    └──────┘    └──┘
src   └──────┘     └──┘
typ   └──────┘    └──┘
605    (λ h, by simp [sqrt_eq_zero'.2, inv_nonpos, h])
id                   └───────────┘    └────────┘  
src             └────┘└───────────┘└──┘└────────┘└┘ 
typ            └────┘└───────────┘└──┘└────────┘└┘
doc             └────┘             └──┘          └┘ 
txt             └────┘             └──┘          └┘ 
par             └────┘             └──┘          └┘ 
pid                              └──┘          └┘ 
st             └────────────────────────────────────┘
606    (λ h, by rw [
id        
src             └────
typ            └────
doc             └────
txt             └────
par             └────
pid               └──
st             └─────
607      ← mul_self_inj_of_nonneg (sqrt_nonneg _) (le_of_lt $ inv_pos $ sqrt_pos.2 h),
id         └────────────────────┘  └─────────┘     └──────┘   └─────┘   └──────┘   
src  ─────┘└────────────────────┘ └─────────┘└──┘ └──────┘ └─────┘ └──────┘└─┘ └──
typ  ─────┘└────────────────────┘ └─────────┘└──┘ └──────┘ └─────┘ └──────┘└─┘└──
doc  ─────┘                                  └──┘                          └─┘ └──
txt  ─────┘                                  └──┘                          └─┘ └──
par  ─────┘                                  └──┘                          └─┘ └──
pid  ─────┘                                  └──┘                          └─┘ └──
st   ───────────────────────────────────────────────────────────────────────────────┘└─
608      mul_self_sqrt (le_of_lt $ inv_pos h), ← mul_inv', mul_self_sqrt (le_of_lt h)])
id       └───────────┘  └──────┘   └─────┘      └──────┘  └───────────┘  └──────┘ 
src  ───┘└───────────┘ └──────┘ └─────┘ └───┘└──────┘└┘└───────────┘ └──────┘ └┘
typ  ───┘└───────────┘ └──────┘ └─────┘└───┘└──────┘└┘└───────────┘ └──────┘└┘
doc  ───┘                               └───┘        └┘                       └┘
txt  ───┘                               └───┘        └┘                       └┘
par  ───┘                               └───┘        └┘                       └┘
pid  ───┘                               └───┘        └┘                       └┘
st   ───────────────────────────────────────┘└──────────┘└──────────────────────────┘
609  
610  @[simp] theorem sqrt_div (hx : 0 ≤ x) (y : ℝ) : sqrt (x / y) = sqrt x / sqrt y :=
id                                                └──┘       └──┘   └──┘ 
src                                                └──┘         └──┘    └──┘
typ                                               └──┘       └──┘   └──┘ 
doc    └──┘
611  by rw [division_def, sqrt_mul hx, sqrt_inv]; refl
id          └──────────┘  └──────┘ └┘  └──────┘
src     └──┘└──────────┘└┘└──────┘  └┘└──────┘  └────
typ     └──┘└──────────┘└┘└──────┘└┘└┘└──────┘  └────
doc     └──┘            └┘          └┘          └────
txt     └──┘            └┘          └┘          └────
par     └──┘            └┘          └┘          └────
pid       └┘            └┘          └┘              
st     └───────────────┘└───────────┘└────────┘└──────
612  
src  
typ  
doc  
txt  
par  
pid  
st   
613  attribute [irreducible] real.le
id                           └─────┘
src                          └─────┘
typ                          └─────┘
doc             └─────────┘
614  
615  end real